CorePatchEnergy

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

The per-core energy split and its pi-measurability

For the Efron–Stein transfer of the fixed-phase observable we must exhibit a genuinely product-measurable observable on the tuple space (↥K → CoeffField d) that agrees Π-almost-everywhere with F_σ ∘ corePatch.

The reconstruction map corePatch is not measurable into the ambient σ-algebra (a raw local event over cubeSet can couple two coordinates through a non-measurable set), so the coarse observable of the glued field cannot be obtained by composing corePatch with a measurable coarse map. The way out is that the coarse observable only sees the glued field through fixed-competitor block-energy integrals, and such an integral splits across the core partition: on the corridor the truncated glued field is the identity (a constant, independent of the tuple), and on each core coreBox ℓ σ k it reads only the single coordinate y k.

This file builds that split. The energy is measured against the elliptically truncated glued field

glueField ℓ σ Θ a := ellipticTruncate Θ (corridorField ℓ σ a),

which is (1, Θ)-elliptic everywhere (needed later for the uniform global bound and the AEE slice) and is a pointwise self-map of coefficient fields.

Main definitions/results:

• glueField, its corridor value and pointwise congruence;
• coreLocalEnergy W X — the block-energy of the glued field over a bounded set W, shown ambient-measurable via the PointwiseLocalSigma W generator trick (this is the measurability heart, using only single-field local events);
• phaseSplitEnergy — the manifestly pi-measurable assembled observable (corridor constant + a finite sum of single-coordinate core energies);
• measurable_phaseSplitEnergy;
• blockEnergyAverage_glueField_corePatch_eq_phaseSplitEnergy — the exact split identity, valid whenever the glued field is (1, Θ)-elliptic on U (which holds Π-a.e. after truncation; supplied by the caller).

The elliptically truncated glued field

noncomputable def HCPolySupport.glueField {d : ℕ} (ℓ : ℝ) (σ : Vec d) (Θ : ℝ) (a : CoeffField d) : CoeffField d

The truncated corridor field fed to the coarse observable: the corridor field corridorField ℓ σ a, then clamped by ellipticTruncate Θ so that every value is (1, Θ)-elliptic. It is a pointwise self-map: its value at x depends on a only through a x.

Equations

• HCPolySupport.glueField ℓ σ Θ a = HCPolySupport.ellipticTruncate Θ (HCPolySupport.corridorField ℓ σ a)

theorem HCPolySupport.glueField_apply_of_mem_corridor {d : ℕ} {ℓ : ℝ} {σ : Vec d} {Θ : ℝ} (hΘ : 1 ≤ Θ) {a : CoeffField d} {x : Vec d} (hx : x ∈ corridorSet ℓ σ) : glueField ℓ σ Θ a x = 1

On the corridor the truncated glued field is the identity (the identity matrix is (1, Θ)-elliptic for Θ ≥ 1).

theorem HCPolySupport.glueField_congr_apply {d : ℕ} {ℓ : ℝ} {σ : Vec d} {Θ : ℝ} {a b : CoeffField d} {x : Vec d} (h : a x = b x) : glueField ℓ σ Θ a x = glueField ℓ σ Θ b x

Pointwise congruence: the value of the glued field at x depends only on a x.

The single-core block energy of the glued field

noncomputable def HCPolySupport.coreLocalEnergy {d : ℕ} (ℓ : ℝ) (σ : Vec d) (Θ : ℝ) (W : Set (Vec d)) (X : BlockState d) (a : CoeffField d) : ℝ

The block energy of the truncated glued field of a, integrated over a set W. When W = coreBox ℓ σ k ∩ U this is the per-core contribution to the coarse energy; it depends on a only through a on W.

Equations

• HCPolySupport.coreLocalEnergy ℓ σ Θ W X a = ∫ (x : HCPolySupport.Vec d) in W, HCPolySupport.blockEnergyDensity (HCPolySupport.glueField ℓ σ Θ a) X x

theorem HCPolySupport.coreLocalEnergy_congr {d : ℕ} {ℓ : ℝ} {σ : Vec d} {Θ : ℝ} {W : Set (Vec d)} (hW : MeasurableSet W) {X : BlockState d} {a b : CoeffField d} (hab : LocalAgreementOn W a b) : coreLocalEnergy ℓ σ Θ W X a = coreLocalEnergy ℓ σ Θ W X b

coreLocalEnergy depends on the field only through its values on W.

theorem HCPolySupport.measurable_coreLocalEnergy {d : ℕ} {ℓ : ℝ} {σ : Vec d} {Θ : ℝ} {W : Set (Vec d)} (hWmeas : MeasurableSet W) (hWbdd : Bornology.IsBounded W) (X : BlockState d) : Measurable fun (a : CoeffField d) => coreLocalEnergy ℓ σ Θ W X a

Measurability heart. coreLocalEnergy is ambient-measurable in the field: it is a single-field bounded-local observable, hence measurable into PointwiseLocalSigma W (via the generator trick) and thus into the ambient σ-algebra. No cross-coordinate coupling is involved — this uses only single-field local events.

The corridor constant and the assembled pi-measurable observable

noncomputable def HCPolySupport.corridorConst {d : ℕ} (ℓ : ℝ) (σ : Vec d) (U : Set (Vec d)) (X : BlockState d) : ℝ

The corridor contribution to the coarse energy: the block energy of the identity field over U ∩ corridorSet. Independent of the tuple.

Equations

• HCPolySupport.corridorConst ℓ σ U X = ∫ (x : HCPolySupport.Vec d) in U ∩ HCPolySupport.corridorSet ℓ σ, HCPolySupport.blockEnergyDensity (fun (x : HCPolySupport.Vec d) => 1) X x

noncomputable def HCPolySupport.phaseSplitEnergy {d : ℕ} (ℓ : ℝ) (σ : Vec d) (Θ : ℝ) (U : Set (Vec d)) (X : BlockState d) (K : Finset (Fin d → ℤ)) (y : ↥K → CoeffField d) : ℝ

The assembled split observable on the tuple space: the corridor constant plus a finite sum of single-coordinate core energies, normalized by 1 / vol U. It is manifestly product-measurable.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.measurable_phaseSplitEnergy {d : ℕ} {ℓ : ℝ} {σ : Vec d} {Θ : ℝ} {U : Set (Vec d)} (hUmeas : MeasurableSet U) (hUbdd : Bornology.IsBounded U) (X : BlockState d) (K : Finset (Fin d → ℤ)) : Measurable fun (y : ↥K → CoeffField d) => phaseSplitEnergy ℓ σ Θ U X K y

Product-measurability of the assembled observable. Each core term is a single-coordinate composition of the ambient-measurable coreLocalEnergy, so the finite sum is measurable for the product σ-algebra MeasurableSpace.pi.

The exact split identity

theorem HCPolySupport.inter_compl_corridorSet_eq_iUnion_coreBox {d : ℕ} {ℓ : ℝ} (hℓ : 0 < ℓ) (σ : Vec d) {U : Set (Vec d)} {K : Finset (Fin d → ℤ)} (hK : ∀ (k : Fin d → ℤ), (coreBox ℓ σ k ∩ U).Nonempty → k ∈ K) : U \ corridorSet ℓ σ = ⋃ (k : ↥K), U ∩ coreBox ℓ σ ↑k

The complement of the corridor, intersected with U, is the disjoint union of the core boxes meeting U.

theorem HCPolySupport.blockEnergyAverage_glueField_corePatch_eq_phaseSplitEnergy {d : ℕ} {ℓ : ℝ} {σ : Vec d} {Θ : ℝ} {U : Set (Vec d)} (hℓ : 0 < ℓ) (hΘ : 1 ≤ Θ) (hUmeas : MeasurableSet U) (X : BlockState d) (hXbl : MemBlockL2 U X.eval) (K : Finset (Fin d → ℤ)) (hK : ∀ (k : Fin d → ℤ), (coreBox ℓ σ k ∩ U).Nonempty → k ∈ K) (y : ↥K → CoeffField d) (hEll : IsEllipticFieldOn 1 Θ U (glueField ℓ σ Θ (corePatch ℓ σ K y))) : blockEnergyAverage U (glueField ℓ σ Θ (corePatch ℓ σ K y)) X = phaseSplitEnergy ℓ σ Θ U X K y

Exact energy split. Whenever the truncated glued field of corePatch ℓ σ K y is (1, Θ)-elliptic on U (so its coarse energy integral converges), the block-energy average splits as the corridor constant plus the per-core single-coordinate energies — i.e. it equals phaseSplitEnergy.