English
Let E be strictly convex and μ a finite measure. If a function f satisfies ‖f(x)‖ ≤ C a.e., then either f equals its μ-average almost everywhere or the norm of its integral is strictly less than μ(real)·C.
Русский
Пусть E строго выпуклоe, μ — конечная мера. Если ‖f(x)‖ ≤ C почти всюду, тогда либо f равно своему среднему значению, либо норма интеграла меньше чем μ(реальное)·C.
LaTeX
$$$\\text{either } f =^\\ae_\\mu \\; \\text{const}_\\alpha\\left(\\langle f\\rangle_\\mu\\right) \\; \\text{or} \\; \\left\\|\\int x\,f(x)\,d\\mu(x)\\right\\| < \\mu(\\mathbb{R})\\,\\cdot\, C$$$
Lean4
/-- If `E` is a strictly convex normed space and `f : α → E` is a function such that `‖f x‖ ≤ C`
a.e., then either this function is a.e. equal to its average value, or the norm of its integral is
strictly less than `μ.real univ * C`. -/
theorem ae_eq_const_or_norm_integral_lt_of_norm_le_const [StrictConvexSpace ℝ E] [IsFiniteMeasure μ]
(h_le : ∀ᵐ x ∂μ, ‖f x‖ ≤ C) : f =ᵐ[μ] const α (⨍ x, f x ∂μ) ∨ ‖∫ x, f x ∂μ‖ < μ.real univ * C :=
by
rcases eq_or_ne μ 0 with h₀ | h₀; · simp [h₀, EventuallyEq]
have hμ : 0 < μ.real univ := by simp [measureReal_def, ENNReal.toReal_pos_iff, pos_iff_ne_zero, h₀, measure_lt_top]
refine (ae_eq_const_or_norm_average_lt_of_norm_le_const h_le).imp_right fun H => ?_
rwa [average_eq, norm_smul, norm_inv, Real.norm_eq_abs, abs_of_pos hμ, ← div_eq_inv_mul, div_lt_iff₀' hμ] at H
