English
Let E be strictly convex and f such that ‖f(x)‖ ≤ C almost everywhere on a finite-measure set t. Theneither f equals its average on t a.e., or the norm of its integral over t is strictly less than μ(t)·C.
Русский
Пусть E строго выпукла и ‖f(x)‖ ≤ C почти всюду на конечном по мере множестве t. Тогда либо f равно своему среднему по t почти всюду, либо нормa интеграла по t строго меньше μ(t)·C.
LaTeX
$$$$ \|\int_t f\, d\mu\| < \mu(t) \cdot C \quad\text{или}\quad f =^a_{t} \text{avg}_t f. $$$$
Lean4
/-- If `E` is a strictly convex normed space and `f : α → E` is a function such that `‖f x‖ ≤ C`
a.e. on a set `t` of finite measure, then either this function is a.e. equal to its average value on
`t`, or the norm of its integral over `t` is strictly less than `μ.real t * C`. -/
theorem ae_eq_const_or_norm_setIntegral_lt_of_norm_le_const [StrictConvexSpace ℝ E] (ht : μ t ≠ ∞)
(h_le : ∀ᵐ x ∂μ.restrict t, ‖f x‖ ≤ C) :
f =ᵐ[μ.restrict t] const α (⨍ x in t, f x ∂μ) ∨ ‖∫ x in t, f x ∂μ‖ < μ.real t * C :=
by
haveI := Fact.mk ht.lt_top
rw [← measureReal_restrict_apply_univ]
exact ae_eq_const_or_norm_integral_lt_of_norm_le_const h_le
