MeasurableObservable

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

The product-measurable observable and its a.e. identity

Building on the per-core split of CorePatchEnergy, this file assembles the genuinely product-measurable observable

rawPhaseObservable … y := 2 · ⨅ n, phaseSplitEnergy … (compₙ) y

where compₙ = canonicalMuGeneratorAffineField P (denseSeq … n) is the canonical countable competitor family used by the Chapter-4 Mu-variational representation. The ⨅ of the pi-measurable per-competitor split energies is pi-measurable, so rawPhaseObservable is measurable for MeasurableSpace.pi — without any measurability of corePatch itself.

The main result is the five-link a.e. identity: for P-a.e. field a,

rawPhaseObservable … (fun k => a|_{coreBox k}) = F_σ(a),

i.e. the product observable, evaluated on the diagonal restriction tuple R a, reproduces the fixed-phase observable exactly. The chain is

1. phaseSplitEnergy compₙ (R a) = blockEnergyAverage U (glued) compₙ (split, CorePatchEnergy),
2. ⨅ₙ blockEnergyAverage U (glued) compₙ = Mu U P glued (mu_eq_iInf …),
3. Mu U P glued = ½ P·𝐀(U; glued) P (mu_eq_half_coarseBlockMatrix_cube, glued is (1,Θ)-elliptic),
4. 𝐀(U; glued) = 𝐀(U; corridorField (corePatch (R a))) (coarseBlockMatrix_congr_of_ae_eq, truncation a.e.),
5. P·𝐀(U; corridorField (corePatch (R a))) P = F_σ(a) (landed phaseObservable_corePatch_restrict_eq).

The genuine spatial measurability of the underlying field — required for the IsEllipticFieldOn hypotheses of links 1 and 3 — is exactly the measurability conjunct of ThetaEllipticLaw (amended 2026-07-22).

The canonical competitor family and the raw product observable

noncomputable def HCPolySupport.phaseCompetitor {d : ℕ} (Q : TriadicCube d) (P : BlockVec d) (n : ℕ) : BlockState d

The n-th canonical Mu-generator competitor on the cube cubeSet Q, the countable dense family used by mu_eq_iInf_blockEnergyAverage_canonicalAEEMuGenerator.

Equations

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

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

The raw product-measurable observable: twice the infimum, over the canonical competitor family, of the per-competitor split energies.

Equations

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

noncomputable def HCPolySupport.phaseObservable {d : ℕ} (ℓ : ℝ) (σ : Vec d) (m : ℤ) (P : BlockVec d) (a : CoeffField d) : ℝ

The fixed-phase observable F_σ(a) = P · 𝐀(U; corridorField ℓ σ a) P.

Equations

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

Product-measurability

theorem HCPolySupport.measurable_rawPhaseObservable {d : ℕ} {ℓ : ℝ} {σ : Vec d} {Θ : ℝ} {m : ℤ} (P : BlockVec d) (K : Finset (Fin d → ℤ)) : Measurable fun (y : ↥K → CoeffField d) => rawPhaseObservable ℓ σ Θ m P K y

Product-measurability of the raw observable. A countable infimum of the pi-measurable per-competitor split energies (measurable_phaseSplitEnergy).

The five-link a.e. identity

theorem HCPolySupport.rawPhaseObservable_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 : CoeffField d) (hbmeas : ∀ (i j : Fin d), Measurable fun (x : Vec d) => b x i j) (hbell : ∀ᵐ (x : Vec d), IsEllipticMatrix 1 Θ (b x)) : (rawPhaseObservable ℓ σ Θ m P K fun (k : ↥K) => restrictCoeffField (coreBox ℓ σ ↑k) b) = phaseObservable ℓ σ m P b

The a.e. identity. For P-a.e. field a (measurable and a.e. (1,Θ)- elliptic, from ThetaEllipticLaw), evaluating the product observable on the diagonal restriction tuple reproduces the fixed-phase observable exactly.

theorem HCPolySupport.rawPhaseObservable_restrict_ae_eq {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) : ∀ᵐ (a : RegCoeffField d) ∂L, (rawPhaseObservable ℓ σ Θ m P K fun (k : ↥K) => restrictCoeffField (coreBox ℓ σ ↑k) a.toFun) = phaseObservable ℓ σ m P a.toFun

The a.e. identity (law form). Corollary of rawPhaseObservable_restrict_eq_of_field under ThetaEllipticLaw, whose measurability + a.e.-ellipticity conjuncts supply the per-field hypotheses.