Documentation

MiscYD.PhD.VCDim.SmallVCImpSmallCondVar

Small VC dimension implies small variance #

This file proves that each marginal of a random variable valued in a small VC dimension set family has small conditional variance conditioned on finitely many other marginals.

References #

theorem small_condVar_of_isNIPWith {Ω : Type u_1} {X : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {A : ΩSet X} {𝓕 : Finset (Set X)} {x : X} {d : } (isNIPWith_𝓕 : IsNIPWith d 𝓕) (hA : ∀ᵐ (ω : Ω) μ, A ω 𝓕) :
ProbabilityTheory.condVar (MeasurableSpace.generateFrom sorry) (fun (ω : Ω) => (A ω).indicator 1 x) μ sorry

If A is a random variable valued in a small VC dimension set family over a fintype X, I ⊆ X is finite and x ∈ I, then x ∈ Ahas small conditional variance conditioned on y ∈ A for each y ∈ I \ {x}.