High-contrast homogenization: Provider.Response.DiagonalWeakNormScaleEnergy

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

Single-scale energy bound for the diagonal weak estimate

The equal-weight partition identity turns the centered child averages into a finite variance. The response maximum controls every child metric, while the partitioned energy of the canonical state closes the resulting square sum.

theorem HCPolySupport.HighContrast.Response.blockAvsumL2_metricRoot_centered_le {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {k t : ℤ} (hkt : k ≤ t) {S : Mat d} {F : Vec d → BlockVec d} (hF₁ : ∀ (i : Fin d), MeasureTheory.IntegrableOn (fun (x : Vec d) => (F x).1 i) (adaptedCell q t) MeasureTheory.volume) (hF₂ : ∀ (i : Fin d), MeasureTheory.IntegrableOn (fun (x : Vec d) => (F x).2 i) (adaptedCell q t) MeasureTheory.volume) : (blockAvsumL2 (alignedIndex q k t) fun (w : Fin d → ℤ) => blockMatVecMul (Book.Ch02.blockDiag S S⁻¹) (blockCellAverage (adaptedCellAt q k w) F - blockCellAverage (adaptedCell q t) F)) ≤ blockAvsumL2 (alignedIndex q k t) fun (w : Fin d → ℤ) => blockMatVecMul (Book.Ch02.blockDiag S S⁻¹) (blockCellAverage (adaptedCellAt q k w) F)

Applying a fixed block metric preserves the finite-variance contraction from child averages to their parent mean.

theorem HCPolySupport.HighContrast.Response.blockAvsumL2_metricRoot_centered_diagonalWeakState_le {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {k t : ℤ} (hkt : k ≤ t) {S : Mat d} {a : CoeffSpace d} (p r : Vec d) : (blockAvsumL2 (alignedIndex q k t) fun (w : Fin d → ℤ) => blockMatVecMul (Book.Ch02.blockDiag S S⁻¹) (blockCellAverage (adaptedCellAt q k w) (diagonalWeakState hq t a p r) - blockCellAverage (adaptedCell q t) (diagonalWeakState hq t a p r))) ≤ blockAvsumL2 (alignedIndex q k t) fun (w : Fin d → ℤ) => blockMatVecMul (Book.Ch02.blockDiag S S⁻¹) (blockCellAverage (adaptedCellAt q k w) (diagonalWeakState hq t a p r))

The canonical diagonal state satisfies the centered finite-variance contraction on every aligned child scale.

theorem HCPolySupport.HighContrast.Response.blockAvsumL2_metricRoot_diagonalWeakState_le {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) {k t : ℤ} (hkt : k ≤ t) {S m : Mat d} (hsymm : matTranspose S = S) (hsq : S * S = m) (hm : Matrix.PosDef m) {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) {rho : ℝ} {a : CoeffSpace d} (p r : Vec d) (hfinite : diagonalWeakMaximum rho q t E a ≠ ⊤) : (blockAvsumL2 (alignedIndex q k t) fun (w : Fin d → ℤ) => blockMatVecMul (Book.Ch02.blockDiag S S⁻¹) (blockCellAverage (adaptedCellAt q k w) (diagonalWeakState hq t a p r))) ≤ √2 * diagonalWeakMetricFactor m E * (1 + √(diagonalWeakMaximum rho q t E a).toReal * 3 ^ (rho * (↑t - ↑k) / 2)) * diagonalWeakEnergy hq t a p r

The uncentered metric square sum on one child scale is controlled by the response maximum and the energy of the canonical parent optimizer.