English
If two nonnegative extended-valued functions satisfy f ≤ᵐμ g, ∫ f dμ < ∞, and ∫ g dμ ≤ ∫ f dμ with g measurable, then f and g are almost everywhere equal.
Русский
Если f ≤ᵐμ g, интеграл f по μ конечен, g измерим, и ∫g ≤ ∫f, тогда f = a.e. g.
LaTeX
$$$(f \\leq_{a.e.}^{μ} g) \\wedge (\\int f dμ \\neq \\infty) \\wedge AEMeasurable\\ g\\ μ \\wedge (\\int g dμ \\le \\int f dμ) \\Rightarrow f =_{μ} g$$$
Lean4
theorem ae_eq_of_ae_le_of_lintegral_le {f g : α → ℝ≥0∞} (hfg : f ≤ᵐ[μ] g) (hf : ∫⁻ x, f x ∂μ ≠ ∞)
(hg : AEMeasurable g μ) (hgf : ∫⁻ x, g x ∂μ ≤ ∫⁻ x, f x ∂μ) : f =ᵐ[μ] g :=
by
have : ∀ n : ℕ, ∀ᵐ x ∂μ, g x < f x + (n : ℝ≥0∞)⁻¹ := by
intro n
simp only [ae_iff, not_lt]
have : ∫⁻ x, f x ∂μ + (↑n)⁻¹ * μ {x : α | f x + (n : ℝ≥0∞)⁻¹ ≤ g x} ≤ ∫⁻ x, f x ∂μ :=
(lintegral_add_mul_meas_add_le_le_lintegral hfg hg n⁻¹).trans hgf
rw [(ENNReal.cancel_of_ne hf).add_le_iff_nonpos_right, nonpos_iff_eq_zero, mul_eq_zero] at this
exact this.resolve_left (ENNReal.inv_ne_zero.2 (ENNReal.natCast_ne_top _))
refine hfg.mp ((ae_all_iff.2 this).mono fun x hlt hle => hle.antisymm ?_)
suffices Tendsto (fun n : ℕ => f x + (n : ℝ≥0∞)⁻¹) atTop (𝓝 (f x)) from ge_of_tendsto' this fun i => (hlt i).le
simpa only [inv_top, add_zero] using tendsto_const_nhds.add (ENNReal.tendsto_inv_iff.2 ENNReal.tendsto_nat_nhds_top)
