English
The set where limRatioMeas hρ x equals 0 has μ-measure zero.
Русский
Множество точек, для которых limRatioMeas hρ x = 0, имеет μ-единицу нулевой меры.
LaTeX
$$$\mu\{x\mid v.limRatioMeas hρ x = 0\} = 0$$$
Lean4
/-- The points with `v.limRatioMeas hρ x = ∞` have measure `0` for `μ`. -/
theorem measure_limRatioMeas_top : μ {x | v.limRatioMeas hρ x = ∞} = 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 = ∞} ∩ 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, 1 ≤ q → μ s ≤ (q : ℝ≥0∞)⁻¹ * ρ s :=
by
intro q hq
rw [mul_comm, ← div_eq_mul_inv, ENNReal.le_div_iff_mul_le _ (Or.inr ρs), mul_comm]
· apply v.mul_measure_le_of_subset_lt_limRatioMeas hρ
intro y hy
have : v.limRatioMeas hρ y = ∞ := hy.1
simp only [this, ENNReal.coe_lt_top, mem_setOf_eq]
· simp only [(zero_lt_one.trans_le hq).ne', true_or, ENNReal.coe_eq_zero, Ne, not_false_iff]
have B : Tendsto (fun q : ℝ≥0 => (q : ℝ≥0∞)⁻¹ * ρ s) atTop (𝓝 (∞⁻¹ * ρ s)) :=
by
apply ENNReal.Tendsto.mul_const _ (Or.inr ρs)
exact ENNReal.tendsto_inv_iff.2 (ENNReal.tendsto_coe_nhds_top.2 tendsto_id)
simp only [zero_mul, ENNReal.inv_top] at B
apply ge_of_tendsto B
exact eventually_atTop.2 ⟨1, A⟩
