ClampedObservable

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

The globally bounded clamped observable

efronStein_transfer_ae_restriction requires the product observable to be globally bounded (∀ y, |G y| ≤ M), not merely a.e. bounded. The raw product observable rawPhaseObservable is only bounded on the a.e. event where the recombined field is elliptic, so we clamp it to [0, C] with C := 2(Θ‖p‖² + ‖q‖²) — the exact C1′ sandwich bound for the coarse quadratic of a (1,Θ)-elliptic field.

The clamp is the identity exactly where it matters: for any measurable, a.e.- (1,Θ)-elliptic field b the truncated glued field glueField ℓ σ Θ b is genuinely (1,Θ)-elliptic on the cube, so phaseObservable ℓ σ m P b ∈ [0, C] (phaseObservable_mem_Icc), and hence clampedPhaseObservable (R b) = phaseObservable b.

Per-field ellipticity and boundedness of the fixed-phase observable

theorem HCPolySupport.isEllipticFieldOn_glueField_of_field {d : ℕ} {ℓ : ℝ} {σ : Vec d} {Θ : ℝ} {m : ℤ} (hΘ : 1 ≤ Θ) {b : CoeffField d} (hbmeas : ∀ (i j : Fin d), Measurable fun (x : Vec d) => b x i j) : IsEllipticFieldOn 1 Θ (cubeSet (originCube d m)) (glueField ℓ σ Θ b)

The truncated glued field of a measurable field is genuinely (1,Θ)-elliptic on the cube.

theorem HCPolySupport.glueField_ae_eq_corridorField {d : ℕ} {ℓ : ℝ} {σ : Vec d} {Θ : ℝ} {m : ℤ} (hΘ : 1 ≤ Θ) {b : CoeffField d} (hbell : ∀ᵐ (x : Vec d), IsEllipticMatrix 1 Θ (b x)) : glueField ℓ σ Θ b =ᵐ[MeasureTheory.volume.restrict (cubeSet (originCube d m))] corridorField ℓ σ b

The truncated glued field agrees a.e. on the cube with the corridor field.

theorem HCPolySupport.phaseObservable_eq_blockVecDot_glueField {d : ℕ} {ℓ : ℝ} {σ : Vec d} {Θ : ℝ} {m : ℤ} (hΘ : 1 ≤ Θ) (P : BlockVec d) {b : CoeffField d} (hbell : ∀ᵐ (x : Vec d), IsEllipticMatrix 1 Θ (b x)) : phaseObservable ℓ σ m P b = blockVecDot P (blockMatVecMul (coarseBlockMatrix (cubeSet (originCube d m)) (glueField ℓ σ Θ b)) P)

The fixed-phase observable equals the coarse quadratic of the truncated glued field (they agree a.e., so the coarse matrices coincide).

theorem HCPolySupport.phaseObservable_mem_Icc {d : ℕ} [NeZero d] {ℓ : ℝ} {σ : Vec d} {Θ : ℝ} {m : ℤ} (hΘ : 1 ≤ Θ) (P : BlockVec d) {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)) : 0 ≤ phaseObservable ℓ σ m P b ∧ phaseObservable ℓ σ m P b ≤ 2 * (Θ * vecNormSq P.1 + vecNormSq P.2)

C1′ bounds for the fixed-phase observable. For any measurable, a.e. (1,Θ)-elliptic field, the observable lands in [0, 2(Θ‖p‖² + ‖q‖²)].

The clamped observable

noncomputable def HCPolySupport.phaseBound {d : ℕ} (Θ : ℝ) (P : BlockVec d) : ℝ

The bound constant C = 2(Θ‖p‖² + ‖q‖²) for the coarse quadratic.

Equations

• HCPolySupport.phaseBound Θ P = 2 * (Θ * HCPolySupport.vecNormSq P.1 + HCPolySupport.vecNormSq P.2)

theorem HCPolySupport.phaseBound_nonneg {d : ℕ} {Θ : ℝ} (hΘ : 1 ≤ Θ) (P : BlockVec d) : 0 ≤ phaseBound Θ P

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

The globally bounded product observable: rawPhaseObservable clamped to [0, phaseBound Θ P].

Equations

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

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

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

The clamped observable is globally bounded by phaseBound Θ P.

theorem HCPolySupport.clampedPhaseObservable_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)) : (clampedPhaseObservable ℓ σ Θ m P K fun (k : ↥K) => restrictCoeffField (coreBox ℓ σ ↑k) b) = phaseObservable ℓ σ m P b

Clamp is the identity on the diagonal. For any measurable, a.e. (1,Θ)-elliptic field b, the clamped observable on the restriction tuple R b equals the fixed-phase observable of b.