English
If s is an affine subspace and x,y,z ∈ P with h : Sbtw R x y z, then s.SOppSide x z follows from the given relations; the preimage along addition by z preserves the SOppSide relation.
Русский
Пусть s — аффинное подпространство, и x,y,z ∈ P; если естьотношение Sbtw x y z, то из этого следует s.SOppSide x z; предобразие по добавлению сохраняет отношение SOppSide.
LaTeX
$$$$ s.SOppSide x z \text{ следует из } h, \text{ предобраз по } x \mapsto z+x \text{ сохраняет } SOppSide. $$$$
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 average value
is strictly less than `C`. -/
theorem ae_eq_const_or_norm_average_lt_of_norm_le_const [StrictConvexSpace ℝ E] (h_le : ∀ᵐ x ∂μ, ‖f x‖ ≤ C) :
f =ᵐ[μ] const α (⨍ x, f x ∂μ) ∨ ‖⨍ x, f x ∂μ‖ < C :=
by
rcases le_or_gt C 0 with hC0 | hC0
· have : f =ᵐ[μ] 0 := h_le.mono fun x hx => norm_le_zero_iff.1 (hx.trans hC0)
simp only [average_congr this, Pi.zero_apply, average_zero]
exact Or.inl this
by_cases hfi : Integrable f μ; swap
· simp [average_eq, integral_undef hfi, hC0]
rcases (le_top : μ univ ≤ ∞).eq_or_lt with hμt | hμt
· simp [average_eq, measureReal_def, hμt, hC0]
haveI : IsFiniteMeasure μ := ⟨hμt⟩
replace h_le : ∀ᵐ x ∂μ, f x ∈ closedBall (0 : E) C := by simpa only [mem_closedBall_zero_iff]
simpa only [interior_closedBall _ hC0.ne', mem_ball_zero_iff] using
(strictConvex_closedBall ℝ (0 : E) C).ae_eq_const_or_average_mem_interior isClosed_closedBall h_le hfi
