Documentation

LeanPool.HighContrastHomogenization.Provider.PolynomialHomogenization.BlockRowGoodTail

High-contrast homogenization: Provider.PolynomialHomogenization.BlockRowGoodTail #

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

Weak-error tails from a quenched block row #

The spatial supremum in the quenched block row is genuinely summable for each coefficient-space sample. On the active source branch, the squared endpoint homogenization error is bounded by that row. Power decay of every later row then gives the finite l¹ weak-error certificate used by large-scale regularity.

source
def HCPolySupport.HighContrast.rowCellExcessSet {d : ℕ} (m n : ℕ) (a : CoeffSpace d) (F : BlockMat d) :
Set ℝ

Excess values over the standard cells at relative generation m - n whose centers lie in the centered cube of generation m.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def HCPolySupport.HighContrast.rowCellExcessSup {d : ℕ} (m n : ℕ) (a : CoeffSpace d) (F : BlockMat d) :
    ℝ

    Supremum of the cell excess values in rowCellExcessSet m n a F.

    Equations
    Instances For
      source
      theorem HCPolySupport.HighContrast.summable_weighted_standardCell_blockExcess_sSup {d : ℕ} [NeZero d] (m : ℕ) (rho : ℝ) (a : CoeffSpace d) (abar : Mat d) (habar : Matrix.PosDef (symmPart abar)) (hrho : 0 < rho) :
      Summable fun (n : ℕ) => 3 ^ (-rho * ↑n) * sSup {r : ℝ | ∃ (w : Fin d → ℤ), standardCellCenter (↑m - ↑n) w ∈ centeredCube d ↑m ∧ r = blockExcess (coarseBlock (standardCell d (↑m - ↑n) w) a) (Book.Ch02.constantBlockMatrix abar)}

      The exact weighted spatial-supremum sequence occurring on the active branch of quenched_block_row is summable.