Documentation

LeanPool.Superdiffusion.Support.Probability.EfronStein.Transfer

Transfer #

Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.

Efron–Stein transfer to coefficient-field laws #

This file transfers the abstract product-space Efron–Stein inequality (Homogenization.efronStein_pi) to a single restriction-unit-range-dependent probability measure P on the honest-fields carrier RegCoeffField d, resampled through a family of restriction endomorphisms.

Fix a Fintype ι and a family of pairwise AreUnitSeparated measurable regions C : ι → Set (Vec d) (the MeasurableSet side-conditions make the carrier restriction σ-algebra RestrictionSigmaR well defined). Writing R a i := restrictReg (C i) (hC i) a for the joint restriction map, each coordinate is a restriction-local random variable for RestrictionSigmaR (C i) (hC i), so the family is independent under a restriction-unit-range-dependent P and the pushforward P.map R factors as the product measure Measure.pi (fun i => P.map (restrictReg (C i) (hC i))). Efron–Stein on that product, transported back through the map identity, yields the variance bound for a bounded measurable observable G of the restricted fields.

The single resampling coordinate is restrictReg (C i) (hC i) a': an independent copy of P re-drawn only on C i.

Reference: the paper (Armstrong–Kuusi–Loher, to appear).

source
noncomputable def HCPolySupport.restrictObservable {d : ℕ} (U : Set (Vec d)) (hU : MeasurableSet U) :
RegCoeffField d → RegCoeffField d

The restriction endomorphism restrictReg U hU, bundled as the identity observable on the U-restricted field. This is the family fed to the carrier independence bridge in the Efron–Stein transfer.

Equations
Instances For
    source
    @[simp]
    theorem HCPolySupport.restrictObservable_apply {d : ℕ} (U : Set (Vec d)) (hU : MeasurableSet U) (a : RegCoeffField d) :
    restrictObservable U hU a = restrictReg U hU a
    source
    theorem HCPolySupport.measurable_restrictObservable {d : ℕ} (U : Set (Vec d)) (hU : MeasurableSet U) :
    Measurable (restrictObservable U hU)

    The restriction observable is (globally) measurable on the carrier.

    source
    theorem HCPolySupport.isRestrictionLocalRandomVariable_restrictObservable {d : ℕ} (U : Set (Vec d)) (hU : MeasurableSet U) :
    Book.Ch04.IsRestrictionLocalRandomVariable U hU (restrictObservable U hU)

    The restriction observable is a restriction-local random variable on its observation set: it is measurable for the carrier restriction σ-algebra RestrictionSigmaR U hU.

    source
    theorem HCPolySupport.efronStein_transfer_restriction {d : ℕ} {ι : Type u_1} [Fintype ι] [DecidableEq ι] {C : ι → Set (Vec d)} (hC : ∀ (i : ι), MeasurableSet (C i)) (hsep : Pairwise fun (i j : ι) => AreUnitSeparated (C i) (C j)) {P : MeasureTheory.Measure (RegCoeffField d)} [MeasureTheory.IsProbabilityMeasure P] (hP : IsRestrictionUnitRangeDependentR P) {G : (ι → RegCoeffField d) → ℝ} (hG : Measurable G) {M : ℝ} (hMG : ∀ (x : ι → RegCoeffField d), |G x| ≤ M) (R : RegCoeffField d → ι → RegCoeffField d) (hRdef : R = fun (a : RegCoeffField d) (i : ι) => restrictReg (C i) ⋯ a) :
    ProbabilityTheory.variance (G ∘ R) P ≤ 1 / 2 * ∑ i : ι, ∫ (a : RegCoeffField d), ∫ (a' : RegCoeffField d), (G (Function.update (R a) i (restrictReg (C i) ⋯ a')) - G (R a)) ^ 2 ∂P ∂P

    Restriction Efron–Stein transfer. For a finite family of pairwise AreUnitSeparated measurable regions C i, a restriction-unit-range-dependent probability measure P on the carrier RegCoeffField d, and a bounded measurable observable G of the jointly restricted fields R a = fun i => restrictReg (C i) (hC i) a, the variance of G ∘ R is controlled by the sum of single-region resampling energies, each an independent copy of P re-drawn only on C i.