English
For locally finite μ and absolutely continuous ρ, ρ(s) ≤ t · μ.withDensity(limRatioMeas hρ) (s) for any t>1 and measurable s.
Русский
Для локально конечной μ и ρ, абсолютно непрерывной по μ, выполняется ρ(s) ≤ t·μ.withDensity(limRatioMeas hρ)(s) для любого t>1 и измеримого s.
LaTeX
$$$\forall s\ MeasurableSet s,\ 1 < t\implies ρ(s) ≤ t \cdot μ.withDensity (v.limRatioMeas hρ) s.$$$
Lean4
/-- The points with `v.limRatioMeas hρ x = 0` have measure `0` for `ρ`. -/
theorem measure_limRatioMeas_zero : ρ {x | v.limRatioMeas hρ x = 0} = 0 :=
by
refine measure_null_of_locally_null _ fun x _ => ?_
obtain ⟨o, xo, o_open, μo⟩ : ∃ o : Set α, x ∈ o ∧ IsOpen o ∧ μ o < ∞ := Measure.exists_isOpen_measure_lt_top μ x
let s := {x : α | v.limRatioMeas hρ x = 0} ∩ o
refine ⟨s, inter_mem_nhdsWithin _ (o_open.mem_nhds xo), le_antisymm ?_ bot_le⟩
have μs : μ s ≠ ∞ := ((measure_mono inter_subset_right).trans_lt μo).ne
have A : ∀ q : ℝ≥0, 0 < q → ρ s ≤ q * μ s := by
intro q hq
apply v.measure_le_mul_of_subset_limRatioMeas_lt hρ
intro y hy
have : v.limRatioMeas hρ y = 0 := hy.1
simp only [this, mem_setOf_eq, hq, ENNReal.coe_pos]
have B : Tendsto (fun q : ℝ≥0 => (q : ℝ≥0∞) * μ s) (𝓝[>] (0 : ℝ≥0)) (𝓝 ((0 : ℝ≥0) * μ s)) :=
by
apply ENNReal.Tendsto.mul_const _ (Or.inr μs)
rw [ENNReal.tendsto_coe]
exact nhdsWithin_le_nhds
simp only [zero_mul, ENNReal.coe_zero] at B
apply ge_of_tendsto B
filter_upwards [self_mem_nhdsWithin] using A
