English
If an integrable function f takes values in a convex set s and the average of f over a subset t with positive measure lies in the interior of s, then the overall average of f lies in the interior of s.
Русский
Если интегрируемая функция f принимает значения в выпуклом множестве s и среднее по некоторому подмножеству t с положительным мерой лежит во внутренности s, то общее среднее f лежит во внутренности s.
LaTeX
$$$$ \left( \frac{1}{\mu(t)} \int_t f \, d\mu
ight) \in \operatorname{int}(s) \quad\Rightarrow\quad \left( \frac{1}{\mu(\Omega)} \int_\Omega f \, d\mu \right) \in \operatorname{int}(s). $$$$
Lean4
/-- If an integrable function `f : α → E` takes values in a convex set `s` and for some set `t` of
positive measure, the average value of `f` over `t` belongs to the interior of `s`, then the average
of `f` over the whole space belongs to the interior of `s`. -/
theorem average_mem_interior_of_set [IsFiniteMeasure μ] (hs : Convex ℝ s) (h0 : μ t ≠ 0) (hfs : ∀ᵐ x ∂μ, f x ∈ s)
(hfi : Integrable f μ) (ht : (⨍ x in t, f x ∂μ) ∈ interior s) : (⨍ x, f x ∂μ) ∈ interior s :=
by
rw [← measure_toMeasurable] at h0; rw [← restrict_toMeasurable (measure_ne_top μ t)] at ht
by_cases h0' : μ (toMeasurable μ t)ᶜ = 0
· rw [← ae_eq_univ] at h0'
rwa [restrict_congr_set h0', restrict_univ] at ht
exact
hs.openSegment_interior_closure_subset_interior ht
(hs.set_average_mem_closure h0' (measure_ne_top _ _) (ae_restrict_of_ae hfs) hfi.integrableOn)
(average_mem_openSegment_compl_self (measurableSet_toMeasurable μ t).nullMeasurableSet h0 h0' hfi)
