English
If f is essentially bounded by C μ-a.e. on s with finite μ(s), then the same bound holds for the integral over s with respect to μ, without requiring s measurability.
Русский
Если f практически ограничена на s константой C μ-почти всюду, то не требуется измеримость s, чтобы не превышать ту же границу нормы интеграла над s.
LaTeX
$$$$ \\left\\| \\int_{x \\in s} f(x) \\, d\\mu(x) \\right\\| \\leq C \\; \\mu_{\\mathbb{R}}(s) $$$$
Lean4
theorem norm_setIntegral_le_of_norm_le_const_ae' {C : ℝ} (hs : μ s < ∞) (hC : ∀ᵐ x ∂μ, x ∈ s → ‖f x‖ ≤ C) :
‖∫ x in s, f x ∂μ‖ ≤ C * μ.real s :=
by
by_cases hfm : AEStronglyMeasurable f (μ.restrict s)
· apply norm_setIntegral_le_of_norm_le_const_ae hs
have A : ∀ᵐ x : X ∂μ, x ∈ s → ‖AEStronglyMeasurable.mk f hfm x‖ ≤ C :=
by
filter_upwards [hC, hfm.ae_mem_imp_eq_mk] with _ h1 h2 h3
rw [← h2 h3]
exact h1 h3
have B : MeasurableSet {x | ‖hfm.mk f x‖ ≤ C} := hfm.stronglyMeasurable_mk.norm.measurable measurableSet_Iic
filter_upwards [hfm.ae_eq_mk, (ae_restrict_iff B).2 A] with _ h1 _
rwa [h1]
· rw [integral_non_aestronglyMeasurable hfm]
have : ∃ᵐ (x : X) ∂μ, x ∈ s := by
apply frequently_ae_mem_iff.mpr
contrapose! hfm
simp [Measure.restrict_eq_zero.mpr hfm]
rcases (this.and_eventually hC).exists with ⟨x, hx, h'x⟩
have : 0 ≤ C := (norm_nonneg _).trans (h'x hx)
simp only [norm_zero, ge_iff_le]
positivity
