Resample

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

One-core resampling stability

The deterministic sensitivity estimate e.fixed.phase.sensitivity behind the Efron–Stein step of Proposition 4.3. Resampling the coefficient field on a single core coreBox ℓ σ k moves the fixed-phase observable F_σ(b) = P · 𝐀(U; b_σ) P by at most a normalized energy over that core:

|F_σ(b) − F_σ(b')| ≤ 48 Θ (vol U)⁻¹ ∫_{coreBox ℓ σ k ∩ U} Z · 𝐀_σ(b) Z,

where Z is a minimizer for corridorField ℓ σ b and b, b' are two fields, (1, Θ)-elliptic on U, agreeing off the core.

The proof specializes the corridor-independent core abs_coarseObservable_sub_le_of_minimizer from PhaseComparison.Stability to the two corridor-modified fields and the core intersection. The field agreement and ellipticity inputs express the resampling-specific geometry; the analytic minimizer assembly has one implementation.

Measurability of a core box

theorem HCPolySupport.measurableSet_coreBox {d : ℕ} (ℓ : ℝ) (σ : Vec d) (k : Fin d → ℤ) : MeasurableSet (coreBox ℓ σ k)

Each core box is measurable (a finite product of closed intervals).

The one-core resampling specialization

theorem HCPolySupport.abs_phaseObservable_resample_sub_le_of_minimizer {d : ℕ} [NeZero d] {Θ : ℝ} (hΘ : 1 ≤ Θ) {m : ℤ} {ℓ : ℝ} {σ : Vec d} {k : Fin d → ℤ} (P : BlockVec d) {b b' : CoeffField d} (hEllb : IsEllipticFieldOn 1 Θ (cubeSet (originCube d m)) b) (hEllb' : IsEllipticFieldOn 1 Θ (cubeSet (originCube d m)) b') (hbb' : Set.EqOn b b' (coreBox ℓ σ k)ᶜ) {Z : BlockState d} (hZadm : IsBlockMuAdmissible (cubeSet (originCube d m)) P Z) (hZresp : BlockResponseSpace (corridorField ℓ σ b) (cubeSet (originCube d m)) Z) (hZeng : Mu (cubeSet (originCube d m)) P (corridorField ℓ σ b) = blockEnergyAverage (cubeSet (originCube d m)) (corridorField ℓ σ b) Z) : |blockVecDot P (blockMatVecMul (coarseBlockMatrix (cubeSet (originCube d m)) (corridorField ℓ σ b')) P) - blockVecDot P (blockMatVecMul (coarseBlockMatrix (cubeSet (originCube d m)) (corridorField ℓ σ b)) P)| ≤ 48 * Θ * (MeasureTheory.volume (cubeSet (originCube d m))).toReal⁻¹ * ∫ (x : Vec d) in coreBox ℓ σ k ∩ cubeSet (originCube d m), blockVecDot (Z.eval x) (blockMatVecMul (blockCoeffField (corridorField ℓ σ b) x) (Z.eval x))

Part 3 (one-core resampling stability), minimizer form. For a fixed grid phase σ and two fields b, b' that are (1, Θ)-elliptic on U := cubeSet (originCube d m) and agree off the core coreBox ℓ σ k, the fixed-phase observable moves by at most a normalized core-energy of the minimizer Z for corridorField ℓ σ b.

theorem HCPolySupport.abs_phaseObservable_resample_sub_le {d : ℕ} [NeZero d] {Θ : ℝ} (hΘ : 1 ≤ Θ) {m : ℤ} {ℓ : ℝ} {σ : Vec d} {k : Fin d → ℤ} (P : BlockVec d) {b b' : CoeffField d} (hEllb : IsEllipticFieldOn 1 Θ (cubeSet (originCube d m)) b) (hEllb' : IsEllipticFieldOn 1 Θ (cubeSet (originCube d m)) b') (hbb' : Set.EqOn b b' (coreBox ℓ σ k)ᶜ) : ∃ (Z : BlockState d), IsBlockMuAdmissible (cubeSet (originCube d m)) P Z ∧ BlockResponseSpace (corridorField ℓ σ b) (cubeSet (originCube d m)) Z ∧ |blockVecDot P (blockMatVecMul (coarseBlockMatrix (cubeSet (originCube d m)) (corridorField ℓ σ b')) P) - blockVecDot P (blockMatVecMul (coarseBlockMatrix (cubeSet (originCube d m)) (corridorField ℓ σ b)) P)| ≤ 48 * Θ * (MeasureTheory.volume (cubeSet (originCube d m))).toReal⁻¹ * ∫ (x : Vec d) in coreBox ℓ σ k ∩ cubeSet (originCube d m), blockVecDot (Z.eval x) (blockMatVecMul (blockCoeffField (corridorField ℓ σ b) x) (Z.eval x))

Part 3 (one-core resampling stability). Existential-minimizer wrapper.