English
The set of points where limRatioMeas hρ x = ∞ has μ-measure zero.
Русский
Мера множества точек, где limRatioMeas hρ x = ∞, равна нулю.
LaTeX
$$$\mu\{x:\ v.limRatioMeas hρ x = ∞\} = 0$$$
Lean4
/-- If, for all `x` in a set `s`, one has frequently `q < ρ a / μ a`, then `q * μ s ≤ ρ s`, as
proved in `measure_le_of_frequently_le`. Since `ρ a / μ a` tends almost everywhere to
`v.limRatioMeas hρ x`, the same property holds for sets `s` on which `q < v.limRatioMeas hρ`. -/
theorem mul_measure_le_of_subset_lt_limRatioMeas {q : ℝ≥0} {s : Set α}
(h : s ⊆ {x | (q : ℝ≥0∞) < v.limRatioMeas hρ x}) : (q : ℝ≥0∞) * μ s ≤ ρ s :=
by
let t := {x : α | Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}
have A : μ tᶜ = 0 := v.ae_tendsto_limRatioMeas hρ
suffices H : (q • μ) (s ∩ t) ≤ ρ (s ∩ t) by
calc
(q • μ) s = (q • μ) (s ∩ t ∪ s ∩ tᶜ) := by rw [inter_union_compl]
_ ≤ (q • μ) (s ∩ t) + (q • μ) (s ∩ tᶜ) := (measure_union_le _ _)
_ ≤ ρ (s ∩ t) + (q • μ) tᶜ := by gcongr; apply inter_subset_right
_ = ρ (s ∩ t) := by simp [A]
_ ≤ ρ s := by gcongr; apply inter_subset_left
refine v.measure_le_of_frequently_le _ (.smul_left .rfl _) _ ?_
intro x hx
have I : ∀ᶠ a in v.filterAt x, (q : ℝ≥0∞) < ρ a / μ a := (tendsto_order.1 hx.2).1 _ (h hx.1)
apply I.frequently.mono fun a ha => ?_
rw [coe_nnreal_smul_apply]
exact ENNReal.mul_le_of_le_div ha.le
