EfronSteinPhase

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

The Efron–Stein bound for the fixed-phase observable

The capstone. Combining the product-measurable clamped observable (ClampedObservable) with the landed a.e.-measurable Efron–Stein transfer (efronStein_transfer_ae_restriction), we obtain the Efron–Stein variance bound for the fixed-phase observable F_σ in the two-field surgery (patchCore) form that the fixed-phase variance assembly consumes.

The two evaluation-point identities are exact tuple identities (no a.e. reasoning): with patchCore the two-field core surgery, Function.update (R a) k (a'|_{coreBox k}) = R (patchCore k a a'), so the resampled observable is literally the diagonal observable of the surgered field. All a.e. reasoning is confined to the single truncation-congruence layer: clampedPhaseObservable (R b) = F_σ(b) for measurable, a.e.-elliptic b (clampedPhaseObservable_restrict_eq_of_field), instantiated at b = a and at b = patchCore k a a' under ThetaEllipticLaw for both draws.

The two-field core surgery

noncomputable def HCPolySupport.patchCore {d : ℕ} (ℓ : ℝ) (σ : Vec d) (j : Fin d → ℤ) (a a' : CoeffField d) : CoeffField d

The two-field core surgery: a' on the core coreBox ℓ σ j, a off it.

Equations

• HCPolySupport.patchCore ℓ σ j a a' x = if x ∈ HCPolySupport.coreBox ℓ σ j then a' x else a x

@[simp]

theorem HCPolySupport.patchCore_apply_of_mem {d : ℕ} {ℓ : ℝ} {σ : Vec d} {j : Fin d → ℤ} {a a' : CoeffField d} {x : Vec d} (hx : x ∈ coreBox ℓ σ j) : patchCore ℓ σ j a a' x = a' x

@[simp]

theorem HCPolySupport.patchCore_apply_of_not_mem {d : ℕ} {ℓ : ℝ} {σ : Vec d} {j : Fin d → ℤ} {a a' : CoeffField d} {x : Vec d} (hx : x ∉ coreBox ℓ σ j) : patchCore ℓ σ j a a' x = a x

theorem HCPolySupport.measurable_patchCore_entry {d : ℕ} {ℓ : ℝ} {σ : Vec d} {j : Fin d → ℤ} {a a' : CoeffField d} (ha : ∀ (i j' : Fin d), Measurable fun (x : Vec d) => a x i j') (ha' : ∀ (i j' : Fin d), Measurable fun (x : Vec d) => a' x i j') (i j' : Fin d) : Measurable fun (x : Vec d) => patchCore ℓ σ j a a' x i j'

theorem HCPolySupport.ae_isEllipticMatrix_patchCore {d : ℕ} {ℓ : ℝ} {σ : Vec d} {Θ : ℝ} {j : Fin d → ℤ} {a a' : CoeffField d} (ha : ∀ᵐ (x : Vec d), IsEllipticMatrix 1 Θ (a x)) (ha' : ∀ᵐ (x : Vec d), IsEllipticMatrix 1 Θ (a' x)) : ∀ᵐ (x : Vec d), IsEllipticMatrix 1 Θ (patchCore ℓ σ j a a' x)

The exact update identity

theorem HCPolySupport.restrictCoeffField_congr {d : ℕ} {U : Set (Vec d)} {f g : CoeffField d} (h : ∀ x ∈ U, f x = g x) : restrictCoeffField U f = restrictCoeffField U g

theorem HCPolySupport.update_restrict_eq_restrict_patchCore {d : ℕ} {ℓ : ℝ} (hℓ : 0 ≤ ℓ) {σ : Vec d} {K : Finset (Fin d → ℤ)} (k : ↥K) (a a' : CoeffField d) : Function.update (fun (k' : ↥K) => restrictCoeffField (coreBox ℓ σ ↑k') a) k (restrictCoeffField (coreBox ℓ σ ↑k) a') = fun (k' : ↥K) => restrictCoeffField (coreBox ℓ σ ↑k') (patchCore ℓ σ (↑k) a a')

Exact update identity. Updating the k-th coordinate of the diagonal restriction tuple by a fresh core-restriction of a' equals the diagonal restriction tuple of the surgered field patchCore k a a' (using core disjointness off k).

The Efron–Stein bound

theorem HCPolySupport.efronStein_patch_abstract {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)) {L : MeasureTheory.Measure (RegCoeffField d)} [MeasureTheory.IsProbabilityMeasure L] (hURD : IsRestrictionUnitRangeDependentR L) {G : (ι → RegCoeffField d) → ℝ} (hG : Measurable G) {M : ℝ} (hMG : ∀ (y : ι → RegCoeffField d), |G y| ≤ M) {Φ : RegCoeffField d → ℝ} {Ψ : ι → RegCoeffField d → RegCoeffField d → ℝ} (hdiag : (G ∘ fun (a : RegCoeffField d) (i : ι) => restrictReg (C i) ⋯ a) =ᵐ[L] Φ) (hupd : ∀ (i : ι), ∀ᵐ (p : RegCoeffField d × RegCoeffField d) ∂L.prod L, G (Function.update ((fun (a : RegCoeffField d) (j : ι) => restrictReg (C j) ⋯ a) p.1) i (restrictReg (C i) ⋯ p.2)) = Ψ i p.1 p.2) : ProbabilityTheory.variance Φ L ≤ 1 / 2 * ∑ i : ι, ∫ (a : RegCoeffField d), ∫ (a' : RegCoeffField d), (Ψ i a a' - Φ a) ^ 2 ∂L ∂L

Abstract Efron–Stein patch transfer (opaque-observable core). For an abstract bounded measurable product observable G on carrier tuples whose diagonal agrees a.e. with Φ and whose single-coordinate resampling agrees a.e. (on the product) with the two-field surgery values Ψ, the Efron–Stein transfer yields the variance bound in surgery form. Keeping G, Φ, Ψ opaque here keeps elaboration at default heartbeats; the fixed-phase instantiation is below.

theorem HCPolySupport.clampedPhaseObservableR_diag_ae {d : ℕ} [NeZero d] {ℓ : ℝ} {σ : Vec d} {Θ : ℝ} {m : ℤ} (hℓ : 0 < ℓ) (hΘ : 1 ≤ Θ) (P : BlockVec d) {L : MeasureTheory.Measure (RegCoeffField d)} (hL : ThetaEllipticLaw Θ L) (K : Finset (Fin d → ℤ)) (hK : ∀ (k : Fin d → ℤ), (coreBox ℓ σ k ∩ cubeSet (originCube d m)).Nonempty → k ∈ K) : ((fun (y : ↥K → RegCoeffField d) => clampedPhaseObservableR ℓ σ Θ m P K y) ∘ fun (a : RegCoeffField d) (k : ↥K) => restrictReg (coreBox ℓ σ ↑k) ⋯ a) =ᵐ[L] fun (a : RegCoeffField d) => phaseObservable ℓ σ m P a.toFun

The diagonal a.e. identity for the carrier clamped observable, in the composed form consumed by efronStein_patch_abstract.

theorem HCPolySupport.clampedPhaseObservableR_update_ae {d : ℕ} [NeZero d] {ℓ : ℝ} {σ : Vec d} {Θ : ℝ} {m : ℤ} (hℓ : 0 < ℓ) (hΘ : 1 ≤ Θ) (P : BlockVec d) {L : MeasureTheory.Measure (RegCoeffField d)} (hL : ThetaEllipticLaw Θ L) (K : Finset (Fin d → ℤ)) (hK : ∀ (k : Fin d → ℤ), (coreBox ℓ σ k ∩ cubeSet (originCube d m)).Nonempty → k ∈ K) (k : ↥K) : ∀ᵐ (p : RegCoeffField d × RegCoeffField d) ∂L.prod L, clampedPhaseObservableR ℓ σ Θ m P K (Function.update ((fun (a : RegCoeffField d) (j : ↥K) => restrictReg (coreBox ℓ σ ↑j) ⋯ a) p.1) k (restrictReg (coreBox ℓ σ ↑k) ⋯ p.2)) = phaseObservable ℓ σ m P (patchCore ℓ σ (↑k) p.1.toFun p.2.toFun)

The single-coordinate resampling identity for the carrier clamped observable: a.e. on the product it equals the fixed-phase observable of the two-field core surgery.

theorem HCPolySupport.efronStein_phaseObservable {d : ℕ} [NeZero d] {ℓ : ℝ} {σ : Vec d} {Θ : ℝ} {m : ℤ} (hℓ : 0 < ℓ) (hΘ : 1 ≤ Θ) (P : BlockVec d) {L : MeasureTheory.Measure (RegCoeffField d)} [MeasureTheory.IsProbabilityMeasure L] (hURD : IsRestrictionUnitRangeDependentR L) (hL : ThetaEllipticLaw Θ L) (K : Finset (Fin d → ℤ)) (hK : ∀ (k : Fin d → ℤ), (coreBox ℓ σ k ∩ cubeSet (originCube d m)).Nonempty → k ∈ K) : ProbabilityTheory.variance (fun (a : RegCoeffField d) => phaseObservable ℓ σ m P a.toFun) L ≤ 1 / 2 * ∑ k : ↥K, ∫ (a : RegCoeffField d), ∫ (a' : RegCoeffField d), (phaseObservable ℓ σ m P (patchCore ℓ σ (↑k) a.toFun a'.toFun) - phaseObservable ℓ σ m P a.toFun) ^ 2 ∂L ∂L

Efron–Stein for the fixed-phase observable. Under a restriction-unit-range-dependent, Θ-elliptic probability law on the carrier, the variance of the fixed-phase observable is controlled by the sum, over the cores meeting the cube, of the two-field core-resampling energies — the patchCore form consumed by the fixed-phase variance assembly. The product-measurable witness is the genuinely carrier-measurable clamped observable clampedPhaseObservableR (CarrierObservable.lean), so the genuine efronStein_transfer_restriction applies (no a.e.-measurability relaxation needed).