High-contrast homogenization: Entry.Annealed.Normalization

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Actual expectation and identity normalization

Finite entrywise expectations commute with deterministic matrix multiplication, so the entrywise integral of the actual coarse block is the annealed block and the entrywise integral of the normalized actual block is the normalized annealed mean. Reading the identity normalizer at one generation fixes the diagonal normalized mean at the doubled identity; the actual block is then centered on its annealed mean, its centered fluctuations have all finite Schatten moments, and a positive actual normalizer keeps the normalized block positive definite. These normalization identities are what the parent--child recurrence p.fixed.geometry.parent.child.recurrence applies to its normalized fluctuation.

theorem HCPolySupport.HighContrast.Annealed.integrable_fullBlock_mul {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {A : CoeffSpace d → BlockMat d} (hA : ∀ (α β : BlockCoord d), MeasureTheory.Integrable (fun (a : CoeffSpace d) => blockMatEntry (A a) α β) P) (B C : FullBlockMat d) (α β : BlockCoord d) : MeasureTheory.Integrable (fun (a : CoeffSpace d) => (B * toFullBlockMat (A a) * C) α β) P

Each entry remains integrable after left and right deterministic multiplication.

theorem HCPolySupport.HighContrast.Annealed.integral_fullBlock_mul {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {A : CoeffSpace d → BlockMat d} (hA : ∀ (α β : BlockCoord d), MeasureTheory.Integrable (fun (a : CoeffSpace d) => blockMatEntry (A a) α β) P) (B C : FullBlockMat d) : (fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), (B * toFullBlockMat (A a) * C) α β ∂P) = (B * Matrix.of fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (A a) α β ∂P) * C

Actual finite entrywise expectation commutes with deterministic matrix products.

theorem HCPolySupport.HighContrast.Annealed.fullBlock_integral_coarseBlock {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (U : Set (Vec d)) : (fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (coarseBlock U a) α β ∂P) = toFullBlockMat (annealedBlock P U)

The annealed matrix is exactly the entrywise integral in full coordinates.

theorem HCPolySupport.HighContrast.Annealed.integral_normalizedBlock_coarseBlock {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {U : Set (Vec d)} (hU : HasIntegrableCoarseBlock P U) (R : BlockMat d) : (ofFullBlockMat fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (normalizedBlock (coarseBlock U a) R) α β ∂P) = normalizedBlock (annealedBlock P U) R

The expectation of the normalized actual block is its normalized actual mean.

theorem HCPolySupport.HighContrast.Annealed.normalizedMean_self (d : ℕ) (hd : 2 ≤ d) (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (γ : ℝ) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ) (hstat : IsStationaryLaw P) (hdag : CoarseEllipticityDagger P γ E Ψ K S) (jStar : ℕ) (hjStar : 2 * d ≤ 3 ^ jStar) (m : Mat d) (hm : Matrix.PosDef m) (j : ℤ) : relMean P (Geometry.explicitRoundedGrid jStar m) j j = Book.Ch02.blockIdentity d

O8: the actual diagonal normalized mean is the doubled identity.

theorem HCPolySupport.HighContrast.Annealed.integral_normalizedBlock_self (d : ℕ) (hd : 2 ≤ d) (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (γ : ℝ) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ) (hstat : IsStationaryLaw P) (hdag : CoarseEllipticityDagger P γ E Ψ K S) (jStar : ℕ) (hjStar : 2 * d ≤ 3 ^ jStar) (m : Mat d) (hm : Matrix.PosDef m) (j : ℤ) : (ofFullBlockMat fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (normalizedBlock (coarseBlock (adaptedCell (Geometry.explicitRoundedGrid jStar m) j) a) (adaptedMean P (Geometry.explicitRoundedGrid jStar m) j)) α β ∂P) = Book.Ch02.blockIdentity d

The diagonal normalized coarse block has identity expectation under the actual law.

theorem HCPolySupport.HighContrast.Annealed.integral_centered_normalized_coarseBlock {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {U : Set (Vec d)} (hU : HasIntegrableCoarseBlock P U) (R : BlockMat d) : (ofFullBlockMat fun (α β : BlockCoord d) => ∫ (a : CoeffSpace d), blockMatEntry (normalizedBlock (blockSub (coarseBlock U a) (annealedBlock P U)) R) α β ∂P) = ofFullBlockMat 0

Centered normalized actual coarse blocks have zero entrywise expectation.

theorem HCPolySupport.HighContrast.Annealed.memLqSchatten_normalizedFluctuation (d : ℕ) (hd : 2 ≤ d) (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (γ : ℝ) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ) (hstat : IsStationaryLaw P) (hdag : CoarseEllipticityDagger P γ E Ψ K S) (jStar : ℕ) (hjStar : 2 * d ≤ 3 ^ jStar) (m : Mat d) (hm : Matrix.PosDef m) (j k : ℤ) (y : Vec d) (N : ℝ) (hN : 1 ≤ N) : SchattenMemLp P N (normalizedFluctuation P (Geometry.explicitRoundedGrid jStar m) j k y)

Every actual fluctuation has all finite Schatten moments, at arbitrary real centers.

theorem HCPolySupport.HighContrast.Annealed.normalizedBlock_posDef {d : ℕ} (F G : BlockMat d) (hF : Matrix.PosDef (toFullBlockMat F)) (hG : Matrix.PosDef (toFullBlockMat G)) : Matrix.PosDef (toFullBlockMat (normalizedBlock F G))

Invertible inverse-root congruence preserves full strict positivity.