English
A convex independent family implies that a point cannot lie in the convex hull of a subset excluding itself.
Русский
Конвексивно независимое семейство означает, что точка не может принадлежать выпуклой оболочке подмножества без самой точки.
LaTeX
$$$\\text{ConvexIndependent}_{\\mathbb{k}}(\\mathrm{Subtype}.val) \\Leftrightarrow \\forall x\\in s, x \\notin convHull( s\\setminus\\{x\\} )$$$
Lean4
/-- If `μ` is a probability measure on `α`, `s` is a convex closed set in `E`, and `f` is an
integrable function sending `μ`-a.e. points to `s`, then the expected value of `f` belongs to `s`:
`∫ x, f x ∂μ ∈ s`. See also `Convex.sum_mem` for a finite sum version of this lemma. -/
theorem integral_mem [IsProbabilityMeasure μ] (hs : Convex ℝ s) (hsc : IsClosed s) (hf : ∀ᵐ x ∂μ, f x ∈ s)
(hfi : Integrable f μ) : (∫ x, f x ∂μ) ∈ s := by
borelize E
rcases hfi.aestronglyMeasurable with ⟨g, hgm, hfg⟩
haveI : SeparableSpace (range g ∩ s : Set E) := (hgm.isSeparable_range.mono inter_subset_left).separableSpace
obtain ⟨y₀, h₀⟩ : (range g ∩ s).Nonempty :=
by
rcases (hf.and hfg).exists with ⟨x₀, h₀⟩
exact ⟨f x₀, by simp only [h₀.2, mem_range_self], h₀.1⟩
rw [integral_congr_ae hfg]; rw [integrable_congr hfg] at hfi
have hg : ∀ᵐ x ∂μ, g x ∈ closure (range g ∩ s) :=
by
filter_upwards [hfg.rw (fun _ y => y ∈ s) hf] with x hx
apply subset_closure
exact ⟨mem_range_self _, hx⟩
set G : ℕ → SimpleFunc α E := SimpleFunc.approxOn _ hgm.measurable (range g ∩ s) y₀ h₀
have : Tendsto (fun n => (G n).integral μ) atTop (𝓝 <| ∫ x, g x ∂μ) :=
tendsto_integral_approxOn_of_measurable hfi _ hg _ (integrable_const _)
refine hsc.mem_of_tendsto this (Eventually.of_forall fun n => hs.sum_mem ?_ ?_ ?_)
· exact fun _ _ => ENNReal.toReal_nonneg
· simp_rw [measureReal_def]
rw [← ENNReal.toReal_sum, (G n).sum_range_measure_preimage_singleton, measure_univ, ENNReal.toReal_one]
exact fun _ _ => measure_ne_top _ _
· simp only [SimpleFunc.mem_range, forall_mem_range]
intro x
apply (range g).inter_subset_right
exact SimpleFunc.approxOn_mem hgm.measurable h₀ _ _
