EfronSteinAE

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

The a.e.-measurable Efron–Stein transfer wrapper

The landed efronStein_transfer_restriction requires a genuinely measurable bounded observable G. The fixed-phase observable of Proposition 4.3, being a coarse quadratic, is only a.e.-strongly-measurable under the resampled product law Π := Measure.pi (fun i => P.map (restrictReg (C i) (hC i))). This file relaxes the measurability hypothesis to AEStronglyMeasurable G Π, keeping the identical Efron–Stein conclusion.

The plumbing:

• clamp a measurable modification Gt of G (via hG.mk) to [-M, M], so it is measurable, everywhere bounded by M, and Gt =ᵐ[Π] G;
• run the landed efronStein_transfer_restriction on Gt;
• transfer the variance (LHS) and each resampling energy (RHS) back to G using the pushforward identities Measure.map R P = Π, Measure.map (·.1 ↦ R) (P ⊗ P) = Π, and the update-resample identity map_update_prod_pi.

The single genuinely new measure-theoretic input is map_update_prod_pi: updating one coordinate of Measure.pi μ by an independent μ i-draw preserves Measure.pi μ.

The update-resample pushforward

theorem HCPolySupport.map_update_prod_pi {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] (i : ι) : MeasureTheory.Measure.map (fun (p : ((j : ι) → α j) × α i) => Function.update p.1 i p.2) ((MeasureTheory.Measure.pi μ).prod (μ i)) = MeasureTheory.Measure.pi μ

Updating coordinate i of a product measure Measure.pi μ by an independent μ i-distributed draw preserves the product measure.

The a.e.-measurable Efron–Stein transfer

theorem HCPolySupport.efronStein_transfer_ae_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 : MeasureTheory.AEStronglyMeasurable G (MeasureTheory.Measure.pi fun (i : ι) => MeasureTheory.Measure.map (restrictReg (C i) ⋯) P)) {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 (a.e. variant). Identical to efronStein_transfer_restriction, but the observable G need only be AEStronglyMeasurable under the resampled product law Π := Measure.pi (fun i => P.map (restrictReg (C i) (hC i))), not genuinely measurable. This is the form consumed by the fixed-phase variance step, whose coarse observable is only a.e.-measurable under a RestrictionLawCarrier.