Coarse-graining support: Support.Book.Ch02.Theorems.WrapAround

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Deterministic wrap-around estimates

This file contains the Chapter 2 deterministic engine behind the wrap-around argument: finite partition subadditivity for coarse block matrices, expressed as a normalized trace defect controlled by the averaged special-coordinate doubled-response J budget.

noncomputable def HCPolySupport.Book.Ch02.fullBlockTrace {d : ℕ} (M : FullBlockMat d) : ℝ

Full-block trace of a finite matrix.

Equations

• HCPolySupport.Book.Ch02.fullBlockTrace M = ∑ α : HCPolySupport.BlockCoord d, M α α

theorem HCPolySupport.Book.Ch02.blockMatLoewnerLE_upperLeft_apply {d : ℕ} {A B : BlockMat d} (h : BlockMatLoewnerLE A B) (i : Fin d) : A.upperLeft i i ≤ B.upperLeft i i

A block Löwner comparison controls diagonal entries of the upper-left block.

theorem HCPolySupport.Book.Ch02.blockMatLoewnerLE_lowerRight_apply {d : ℕ} {A B : BlockMat d} (h : BlockMatLoewnerLE A B) (i : Fin d) : A.lowerRight i i ≤ B.lowerRight i i

A block Löwner comparison controls diagonal entries of the lower-right block.

noncomputable def HCPolySupport.Book.Ch02.specialCoordinateBlockJTraceBudget {d : ℕ} (σ : ℝ) (A : BlockMat d) : ℝ

The diagonal block-J trace budget associated with the special coordinate probes (σ^{-1/2} e_i, σ^{1/2} e_i), written directly in terms of a block matrix.

Equations

• HCPolySupport.Book.Ch02.specialCoordinateBlockJTraceBudget σ A = ∑ i : Fin d, (1 / 2 * (σ⁻¹ * A.upperLeft i i) + 1 / 2 * (σ * A.lowerRight i i) - 1)

theorem HCPolySupport.Book.Ch02.specialCoordinateBlockJTraceBudget_sub {d : ℕ} (σ : ℝ) (A B : BlockMat d) : specialCoordinateBlockJTraceBudget σ B - specialCoordinateBlockJTraceBudget σ A = ∑ i : Fin d, (1 / 2 * (σ⁻¹ * (B.upperLeft i i - A.upperLeft i i)) + 1 / 2 * (σ * (B.lowerRight i i - A.lowerRight i i)))

theorem HCPolySupport.Book.Ch02.normalizedBlockSubTrace_le_specialCoordinateBlockJTraceBudget {d : ℕ} {A B : BlockMat d} {σ : ℝ} (r : BlockCoord d → ℝ) (hAB : BlockMatLoewnerLE A B) (hrUpper : ∀ (i : Fin d), r (Sum.inl i) * r (Sum.inl i) ≤ σ⁻¹) (hrLower : ∀ (i : Fin d), r (Sum.inr i) * r (Sum.inr i) ≤ σ) (hParentBudget_nonneg : 0 ≤ specialCoordinateBlockJTraceBudget σ A) : fullBlockTrace (Matrix.diagonal r * (toFullBlockMat B - toFullBlockMat A) * Matrix.diagonal r) ≤ 2 * specialCoordinateBlockJTraceBudget σ B

The normalized trace of a positive block additivity defect is controlled by the special-coordinate trace budget of the upper matrix.

theorem HCPolySupport.Book.Ch02.sum_doubledResponseJ_coordinateScales_eq_specialCoordinateBlockJTraceBudget {d : ℕ} (U : Domain d) (a : CoeffOn U) {σ cp cq : ℝ} (hcp2 : cp * cp = σ⁻¹) (hcq2 : cq * cq = σ) (hcpq : cp * cq = 1) : ∑ i : Fin d, doubledResponseJ U a (cp • Pi.single i 1, 0) (cq • Pi.single i 1, 0) = specialCoordinateBlockJTraceBudget σ (coarseBlockMatrix U a)

theorem HCPolySupport.Book.Ch02.specialCoordinateBlockJTraceBudget_weightedBlockAverage {d : ℕ} {U : Domain d} (Pcell : DomainPartition U) (σ : ℝ) (F : Pcell.Cell → BlockMat d) : specialCoordinateBlockJTraceBudget σ (Pcell.weightedBlockAverage F) = Pcell.weightedAverage fun (c : Pcell.Cell) => specialCoordinateBlockJTraceBudget σ (F c)

The special-coordinate block-J trace budget commutes with a finite partition average.

theorem HCPolySupport.Book.Ch02.isSymmetricBlockMat_weightedBlockAverage {d : ℕ} {U : Domain d} (Pcell : DomainPartition U) (F : Pcell.Cell → BlockMat d) (hF : ∀ (c : Pcell.Cell), IsSymmetricBlockMat (F c)) : IsSymmetricBlockMat (Pcell.weightedBlockAverage F)

Weighted averages of symmetric block matrices remain symmetric.

theorem HCPolySupport.Book.Ch02.weightedBlockAverage_wrapAround_normalizedTrace_le_specialCoordinateDoubledResponseJ {d : ℕ} {U : Domain d} (a : CoeffOn U) (Pcell : DomainPartition U) (aCell : (c : Pcell.Cell) → CoeffOn (Pcell.cell c)) (hcell : ∀ (c : Pcell.Cell), a.RestrictsTo (aCell c)) {σ cp cq : ℝ} (hcp2 : cp * cp = σ⁻¹) (hcq2 : cq * cq = σ) (hcpq : cp * cq = 1) (r : BlockCoord d → ℝ) (hrUpper : ∀ (i : Fin d), r (Sum.inl i) * r (Sum.inl i) ≤ σ⁻¹) (hrLower : ∀ (i : Fin d), r (Sum.inr i) * r (Sum.inr i) ≤ σ) : have A := coarseBlockMatrix U a; have B := Pcell.weightedBlockAverage fun (c : Pcell.Cell) => coarseBlockMatrix (Pcell.cell c) (aCell c); have J := Pcell.weightedAverage fun (c : Pcell.Cell) => ∑ i : Fin d, doubledResponseJ (Pcell.cell c) (aCell c) (cp • Pi.single i 1, 0) (cq • Pi.single i 1, 0); fullBlockTrace (Matrix.diagonal r * (toFullBlockMat B - toFullBlockMat A) * Matrix.diagonal r) ≤ 2 * J

Main deterministic wrap-around engine: the normalized trace defect between a parent coarse block matrix and the weighted average of its children is controlled by the averaged special-coordinate doubled-response budget.