CarrierObservable

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

The carrier-measurable clamped observable

The shipped fixed-phase Efron–Stein chain exhibited a product-measurable observable on the raw tuple space (↥K → CoeffField d) via the fine PointwiseLocalSigma generator trick (measurable_coreLocalEnergy). On the honest carrier that trick is unavailable (fine local events are not carrier events), and the truncated per-core energy is a genuinely nonlinear functional of the field, so its entry-test lane is not a transported generator.

This file replaces that measurability heart with an honest carrier construction:

• coreWindow — the open core window (open interior box ∩ open cube), whose difference from the half-open core piece coreBox ∩ cubeSet is Lebesgue-null;
• coreGoodSet — the genuinely measurable event (a slicePart rational-ball intersection, Packet P4b) that the field is a.e. (1,Θ)-elliptic on the core window;
• coreLocalEnergyR — the per-core energy of the truncated glued field, totalized by 0 off coreGoodSet;
• measurable_coreLocalEnergyR — the measurability heart: on coreGoodSet the truncation is a.e. invisible, so the energy decomposes as a corridor constant plus an indicator-weighted block-coefficient integral over the open window, measurable through the carrier L² realization engine of CarrierMuFamily (dense-probe inner products = localized entryTestR generators);
• phaseSplitEnergyR, rawPhaseObservableR, clampedPhaseObservableR — the assembled genuinely product-measurable clamped observable on carrier tuples;
• clampedPhaseObservableR_restrict_eq_of_field — the diagonal identity: on the carrier restriction tuple of a measurable, a.e. (1,Θ)-elliptic field it reproduces the fixed-phase observable exactly (via the shipped raw five-link identity).

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

The open core window and its null boundary

def HCPolySupport.coreBoxIoo {d : ℕ} (ℓ : ℝ) (σ : Vec d) (k : Fin d → ℤ) : Set (Vec d)

The open interior box of coreBox (product of open intervals).

Equations

• HCPolySupport.coreBoxIoo ℓ σ k = Set.univ.pi fun (i : Fin d) => Set.Ioo (σ i + ↑(k i) * ℓ + 1) (σ i + (↑(k i) + 1) * ℓ - 1)

theorem HCPolySupport.coreBoxIoo_subset_coreBox {d : ℕ} {ℓ : ℝ} {σ : Vec d} {k : Fin d → ℤ} : coreBoxIoo ℓ σ k ⊆ coreBox ℓ σ k

theorem HCPolySupport.isOpen_coreBoxIoo {d : ℕ} (ℓ : ℝ) (σ : Vec d) (k : Fin d → ℤ) : IsOpen (coreBoxIoo ℓ σ k)

theorem HCPolySupport.coreBox_ae_eq_coreBoxIoo {d : ℕ} (ℓ : ℝ) (σ : Vec d) (k : Fin d → ℤ) : coreBox ℓ σ k =ᵐ[MeasureTheory.volume] coreBoxIoo ℓ σ k

The closed core box agrees with its open interior box up to a null set.

def HCPolySupport.coreWindow {d : ℕ} (ℓ : ℝ) (σ : Vec d) (k : Fin d → ℤ) (m : ℤ) : Set (Vec d)

The open core window: interior box ∩ open cube.

Equations

• HCPolySupport.coreWindow ℓ σ k m = HCPolySupport.coreBoxIoo ℓ σ k ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)

theorem HCPolySupport.isOpen_coreWindow {d : ℕ} (ℓ : ℝ) (σ : Vec d) (k : Fin d → ℤ) (m : ℤ) : IsOpen (coreWindow ℓ σ k m)

theorem HCPolySupport.measurableSet_coreWindow {d : ℕ} (ℓ : ℝ) (σ : Vec d) (k : Fin d → ℤ) (m : ℤ) : MeasurableSet (coreWindow ℓ σ k m)

theorem HCPolySupport.coreWindow_subset_cubeSet {d : ℕ} {ℓ : ℝ} {σ : Vec d} {k : Fin d → ℤ} {m : ℤ} : coreWindow ℓ σ k m ⊆ cubeSet (originCube d m)

theorem HCPolySupport.coreWindow_subset_coreBox {d : ℕ} {ℓ : ℝ} {σ : Vec d} {k : Fin d → ℤ} {m : ℤ} : coreWindow ℓ σ k m ⊆ coreBox ℓ σ k

theorem HCPolySupport.corePiece_ae_eq_coreWindow {d : ℕ} (ℓ : ℝ) (σ : Vec d) (k : Fin d → ℤ) (m : ℤ) : coreBox ℓ σ k ∩ cubeSet (originCube d m) =ᵐ[MeasureTheory.volume] coreWindow ℓ σ k m

The half-open core piece agrees with the open core window up to a null set.

theorem HCPolySupport.isFiniteMeasure_volumeMeasureOn_coreWindow {d : ℕ} (ℓ : ℝ) (σ : Vec d) (k : Fin d → ℤ) (m : ℤ) : MeasureTheory.IsFiniteMeasure (volumeMeasureOn (coreWindow ℓ σ k m))

theorem HCPolySupport.isFiniteMeasure_volumeMeasureOn_corePiece {d : ℕ} (ℓ : ℝ) (σ : Vec d) (k : Fin d → ℤ) (m : ℤ) : MeasureTheory.IsFiniteMeasure (volumeMeasureOn (coreBox ℓ σ k ∩ cubeSet (originCube d m)))

The good event

def HCPolySupport.coreGoodSet {d : ℕ} (ℓ : ℝ) (σ : Vec d) (Θ : ℝ) (k : Fin d → ℤ) (m : ℤ) : Set (RegCoeffField d)

The genuinely measurable good event: the field is a.e. (1,Θ)-elliptic on the open core window (as a slicePart rational-ball intersection).

Equations

• HCPolySupport.coreGoodSet ℓ σ Θ k m = HCPolySupport.slicePart (HCPolySupport.coreWindow ℓ σ k m) 1 Θ

theorem HCPolySupport.measurableSet_coreGoodSet {d : ℕ} (ℓ : ℝ) (σ : Vec d) (Θ : ℝ) (k : Fin d → ℤ) (m : ℤ) : MeasurableSet (coreGoodSet ℓ σ Θ k m)

theorem HCPolySupport.mem_coreGoodSet_iff {d : ℕ} {ℓ : ℝ} {σ : Vec d} {Θ : ℝ} {k : Fin d → ℤ} {m : ℤ} {b : RegCoeffField d} : b ∈ coreGoodSet ℓ σ Θ k m ↔ ∀ᵐ (x : Vec d) ∂MeasureTheory.volume.restrict (coreWindow ℓ σ k m), IsEllipticMatrix 1 Θ (b.toFun x)

Membership in the good event is exactly a.e. (1,Θ)-ellipticity on the open core window.

theorem HCPolySupport.ae_isEllipticMatrix_corePiece_of_mem_coreGoodSet {d : ℕ} {ℓ : ℝ} {σ : Vec d} {Θ : ℝ} {k : Fin d → ℤ} {m : ℤ} {b : RegCoeffField d} (hb : b ∈ coreGoodSet ℓ σ Θ k m) : ∀ᵐ (x : Vec d) ∂MeasureTheory.volume.restrict (coreBox ℓ σ k ∩ cubeSet (originCube d m)), IsEllipticMatrix 1 Θ (b.toFun x)

On the good event, the field is a.e. (1,Θ)-elliptic on the half-open core piece as well (null boundary).

noncomputable def HCPolySupport.thetaSliceLevel (Θ : ℝ) : ℕ

The slice level attached to the ellipticity constant Θ.

Equations

• HCPolySupport.thetaSliceLevel Θ = ⌈Θ⌉₊

theorem HCPolySupport.aeeSlice_coreWindow_of_mem_coreGoodSet {d : ℕ} {ℓ : ℝ} {σ : Vec d} {Θ : ℝ} {k : Fin d → ℤ} {m : ℤ} {b : RegCoeffField d} (hb : b ∈ coreGoodSet ℓ σ Θ k m) : AEEQuantitativeEllipticSlice (coreWindow ℓ σ k m) (thetaSliceLevel Θ) b.toFun

On the good event, the field lies in the AEE quantitative slice of the open core window at level ⌈Θ⌉₊.

The totalized per-core energy

noncomputable def HCPolySupport.coreLocalEnergyR {d : ℕ} (ℓ : ℝ) (σ : Vec d) (Θ : ℝ) (m : ℤ) (X : BlockState d) (k : Fin d → ℤ) (b : RegCoeffField d) : ℝ

The per-core energy of the truncated glued field, totalized by 0 off the genuinely measurable good event.

Equations

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

theorem HCPolySupport.coreLocalEnergyR_of_mem {d : ℕ} {ℓ : ℝ} {σ : Vec d} {Θ : ℝ} {m : ℤ} {X : BlockState d} {k : Fin d → ℤ} {b : RegCoeffField d} (hb : b ∈ coreGoodSet ℓ σ Θ k m) : coreLocalEnergyR ℓ σ Θ m X k b = coreLocalEnergy ℓ σ Θ (coreBox ℓ σ k ∩ cubeSet (originCube d m)) X b.toFun

The decomposition on the good event

theorem HCPolySupport.isEllipticFieldOn_glueField_of_field_set {d : ℕ} {ℓ : ℝ} {σ : Vec d} {Θ : ℝ} {W : Set (Vec d)} (hW : MeasurableSet W) (hΘ : 1 ≤ Θ) {b : CoeffField d} (hbmeas : ∀ (i j : Fin d), Measurable fun (x : Vec d) => b x i j) : IsEllipticFieldOn 1 Θ W (glueField ℓ σ Θ b)

The truncated glued field of an entrywise-measurable field is genuinely (1,Θ)-elliptic on any measurable set (general-W version of the cube statement in ClampedObservable).

theorem HCPolySupport.coreLocalEnergy_eq_corridorPiece_add_sum {d : ℕ} {ℓ : ℝ} {σ : Vec d} {Θ : ℝ} (hΘ : 1 ≤ Θ) {m : ℤ} (X : BlockState d) (hX : MemBlockL2 (cubeSet (originCube d m)) X.eval) {k : Fin d → ℤ} {b : RegCoeffField d} (hb : b ∈ coreGoodSet ℓ σ Θ k m) : coreLocalEnergy ℓ σ Θ (coreBox ℓ σ k ∩ cubeSet (originCube d m)) X b.toFun = (∫ (x : Vec d) in coreBox ℓ σ k ∩ cubeSet (originCube d m) ∩ corridorSet ℓ σ, blockEnergyDensity (fun (x : Vec d) => 1) X x) + ∑ α : BlockCoord d, ∑ β : BlockCoord d, ∫ (x : Vec d) in coreWindow ℓ σ k m, ((coreBox ℓ σ k ∩ cubeSet (originCube d m)) \ corridorSet ℓ σ).indicator (blockEnergyEntryWeight X α β) x * toFullBlockMat (blockCoeffField b.toFun x) α β

The decomposition of the per-core energy on the good event. The truncation is invisible off the corridor, so the energy is a corridor constant plus an indicator-weighted sum of block-coefficient entry integrals over the open core window.

The measurability heart

theorem HCPolySupport.measurable_coreLocalEnergyR {d : ℕ} {ℓ : ℝ} {σ : Vec d} {Θ : ℝ} (hΘ : 1 ≤ Θ) {m : ℤ} (X : BlockState d) (hX : MemBlockL2 (cubeSet (originCube d m)) X.eval) (k : Fin d → ℤ) : Measurable (coreLocalEnergyR ℓ σ Θ m X k)

The totalized per-core energy is genuinely measurable on the carrier. On the good event the energy is a corridor constant plus indicator-weighted block-coefficient entry integrals over the open core window, each measurable through the carrier L² realization engine; off the good event it is 0, and the good event itself is genuinely measurable (slicePart).

The assembled carrier observables

noncomputable def HCPolySupport.phaseSplitEnergyR {d : ℕ} (ℓ : ℝ) (σ : Vec d) (Θ : ℝ) (m : ℤ) (X : BlockState d) (K : Finset (Fin d → ℤ)) (y : ↥K → RegCoeffField d) : ℝ

The carrier split observable: corridor constant plus totalized per-core energies, normalized by the cube volume.

Equations

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

theorem HCPolySupport.measurable_phaseSplitEnergyR {d : ℕ} {ℓ : ℝ} {σ : Vec d} {Θ : ℝ} (hΘ : 1 ≤ Θ) {m : ℤ} (X : BlockState d) (hX : MemBlockL2 (cubeSet (originCube d m)) X.eval) (K : Finset (Fin d → ℤ)) : Measurable fun (y : ↥K → RegCoeffField d) => phaseSplitEnergyR ℓ σ Θ m X K y

theorem HCPolySupport.phaseSplitEnergyR_eq_of_good {d : ℕ} {ℓ : ℝ} {σ : Vec d} {Θ : ℝ} {m : ℤ} (X : BlockState d) {K : Finset (Fin d → ℤ)} {y : ↥K → RegCoeffField d} (hy : ∀ (k : ↥K), y k ∈ coreGoodSet ℓ σ Θ (↑k) m) : phaseSplitEnergyR ℓ σ Θ m X K y = phaseSplitEnergy ℓ σ Θ (cubeSet (originCube d m)) X K fun (k : ↥K) => (y k).toFun

On tuples of good coordinates the carrier split observable agrees with the raw split observable of the underlying fields.

noncomputable def HCPolySupport.rawPhaseObservableR {d : ℕ} (ℓ : ℝ) (σ : Vec d) (Θ : ℝ) (m : ℤ) (P : BlockVec d) (K : Finset (Fin d → ℤ)) (y : ↥K → RegCoeffField d) : ℝ

The carrier raw observable: twice the infimum over the canonical competitor family of the carrier split energies.

Equations

• HCPolySupport.rawPhaseObservableR ℓ σ Θ m P K y = 2 * ⨅ (n : ℕ), HCPolySupport.phaseSplitEnergyR ℓ σ Θ m (HCPolySupport.phaseCompetitor (HCPolySupport.originCube d m) P n) K y

theorem HCPolySupport.measurable_rawPhaseObservableR {d : ℕ} {ℓ : ℝ} {σ : Vec d} {Θ : ℝ} (hΘ : 1 ≤ Θ) {m : ℤ} (P : BlockVec d) (K : Finset (Fin d → ℤ)) : Measurable fun (y : ↥K → RegCoeffField d) => rawPhaseObservableR ℓ σ Θ m P K y

theorem HCPolySupport.rawPhaseObservableR_eq_of_good {d : ℕ} {ℓ : ℝ} {σ : Vec d} {Θ : ℝ} {m : ℤ} (P : BlockVec d) {K : Finset (Fin d → ℤ)} {y : ↥K → RegCoeffField d} (hy : ∀ (k : ↥K), y k ∈ coreGoodSet ℓ σ Θ (↑k) m) : rawPhaseObservableR ℓ σ Θ m P K y = rawPhaseObservable ℓ σ Θ m P K fun (k : ↥K) => (y k).toFun

On tuples of good coordinates the carrier raw observable agrees with the raw one.

noncomputable def HCPolySupport.clampedPhaseObservableR {d : ℕ} (ℓ : ℝ) (σ : Vec d) (Θ : ℝ) (m : ℤ) (P : BlockVec d) (K : Finset (Fin d → ℤ)) (y : ↥K → RegCoeffField d) : ℝ

The carrier clamped observable.

Equations

• HCPolySupport.clampedPhaseObservableR ℓ σ Θ m P K y = max 0 (min (HCPolySupport.phaseBound Θ P) (HCPolySupport.rawPhaseObservableR ℓ σ Θ m P K y))

theorem HCPolySupport.measurable_clampedPhaseObservableR {d : ℕ} {ℓ : ℝ} {σ : Vec d} {Θ : ℝ} (hΘ : 1 ≤ Θ) {m : ℤ} (P : BlockVec d) (K : Finset (Fin d → ℤ)) : Measurable fun (y : ↥K → RegCoeffField d) => clampedPhaseObservableR ℓ σ Θ m P K y

theorem HCPolySupport.abs_clampedPhaseObservableR_le {d : ℕ} {ℓ : ℝ} {σ : Vec d} {Θ : ℝ} {m : ℤ} (hΘ : 1 ≤ Θ) (P : BlockVec d) (K : Finset (Fin d → ℤ)) (y : ↥K → RegCoeffField d) : |clampedPhaseObservableR ℓ σ Θ m P K y| ≤ phaseBound Θ P

The carrier clamped observable is globally bounded by phaseBound Θ P.

theorem HCPolySupport.clampedPhaseObservableR_eq_of_good {d : ℕ} {ℓ : ℝ} {σ : Vec d} {Θ : ℝ} {m : ℤ} (P : BlockVec d) {K : Finset (Fin d → ℤ)} {y : ↥K → RegCoeffField d} (hy : ∀ (k : ↥K), y k ∈ coreGoodSet ℓ σ Θ (↑k) m) : clampedPhaseObservableR ℓ σ Θ m P K y = clampedPhaseObservable ℓ σ Θ m P K fun (k : ↥K) => (y k).toFun

On tuples of good coordinates the carrier clamped observable agrees with the raw clamped observable of the underlying fields.

The diagonal identity

theorem HCPolySupport.restrictReg_toFun_eq {d : ℕ} (U : Set (Vec d)) (hU : MeasurableSet U) (b : RegCoeffField d) : (restrictReg U hU b).toFun = restrictCoeffField U b.toFun

The toFun of the carrier restriction is the raw restriction of the toFun.

theorem HCPolySupport.restrictReg_mem_coreGoodSet {d : ℕ} {ℓ : ℝ} {σ : Vec d} {Θ : ℝ} {m : ℤ} {k : Fin d → ℤ} {b : RegCoeffField d} (hbell : ∀ᵐ (x : Vec d), IsEllipticMatrix 1 Θ (b.toFun x)) : restrictReg (coreBox ℓ σ k) ⋯ b ∈ coreGoodSet ℓ σ Θ k m

The carrier restriction of a globally a.e.-(1,Θ)-elliptic field to a core box lies in the good event of that core.

theorem HCPolySupport.clampedPhaseObservableR_restrict_eq_of_field {d : ℕ} [NeZero d] {ℓ : ℝ} {σ : Vec d} {Θ : ℝ} {m : ℤ} (hℓ : 0 < ℓ) (hΘ : 1 ≤ Θ) (P : BlockVec d) (K : Finset (Fin d → ℤ)) (hK : ∀ (k : Fin d → ℤ), (coreBox ℓ σ k ∩ cubeSet (originCube d m)).Nonempty → k ∈ K) (b : RegCoeffField d) (hbell : ∀ᵐ (x : Vec d), IsEllipticMatrix 1 Θ (b.toFun x)) : (clampedPhaseObservableR ℓ σ Θ m P K fun (k : ↥K) => restrictReg (coreBox ℓ σ ↑k) ⋯ b) = phaseObservable ℓ σ m P b.toFun

The diagonal identity. On the carrier restriction tuple of a (globally) a.e.-(1,Θ)-elliptic carrier field, the carrier clamped observable reproduces the fixed-phase observable exactly.