Documentation

LeanPool.HighContrastHomogenization.Provider.Quenched.PhysicalScaleBlockRow

High-contrast homogenization: Provider.Quenched.PhysicalScaleBlockRow #

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

Physical-scale covariance of the quenched block row #

The weighted row of normalized coarse-block excesses is unchanged when the hatted coefficient and restored source scale are pulled back to the original sample. Every inner generation and the outer containing cube shift by the same restoration depth.

noncomputable def HCPolySupport.HighContrast.Quenched.quenchedBlockRow {d : ℕ} (rho : ℝ) (Abar : BlockMat d) (sourceScale : ℝ) (a : CoeffSpace d) (m : ℕ) :

The weighted spatial row of normalized coarse-block excesses at a natural outer generation. The source scale is a pointwise scalar so the same row can be evaluated before or after a change of coefficient coordinates.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    theorem HCPolySupport.HighContrast.Quenched.quenched_block_row_physical_scale_coeff {d : ℕ} (rho : ℝ) (Abar : BlockMat d) (sourceScale : ℝ) (N m : ℕ) (a : CoeffSpace d) :
    quenchedBlockRow rho Abar (max 1 (sourceScale / 3 ^ N)) (physicalScaleCoefficient N a) m = quenchedBlockRow rho Abar sourceScale a (N + m)

    Pulling the hatted row back to the original sample shifts every coarse generation by N and restores the unfloored source scale exactly.