High-contrast homogenization: Provider.Quenched.EndpointRelativeBlockRow

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

Structural properties of the endpoint-relative block row

The quenched replay uses the same spatial row after changing to the units of the annealed endpoint. This file supplies the structural facts about that row: measurability, nonnegativity, pointwise summability, and a measurable weighted tail representative. The quantitative decay is kept separate.

theorem HCPolySupport.HighContrast.Quenched.quenched_block_row_max_one_source {d : ℕ} (rho : ℝ) (F : BlockMat d) (sourceScale : ℝ) (a : CoeffSpace d) (m : ℕ) : quenchedBlockRow rho F (max 1 sourceScale) a m = quenchedBlockRow rho F sourceScale a m

Flooring the source scale at one does not change a row indexed by a natural generation.

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

Excess values over 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.

noncomputable def HCPolySupport.HighContrast.Quenched.endpointCellExcessSup {d : ℕ} (m n : ℕ) (a : CoeffSpace d) (F : BlockMat d) : ℝ

Supremum of the excess values in endpointCellExcessSet m n a F.

Equations

• HCPolySupport.HighContrast.Quenched.endpointCellExcessSup m n a F = sSup (HCPolySupport.HighContrast.Quenched.endpointCellExcessSet m n a F)

theorem HCPolySupport.HighContrast.Quenched.quenched_block_row_nonneg {d : ℕ} [NeZero d] {F : BlockMat d} (hF : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) (rho sourceScale : ℝ) (a : CoeffSpace d) (m : ℕ) : 0 ≤ quenchedBlockRow rho F sourceScale a m

Every endpoint-relative block row is nonnegative.

theorem HCPolySupport.HighContrast.Quenched.summable_endpoint_block_row {d : ℕ} [NeZero d] {F : BlockMat d} (hF : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) {rho : ℝ} (hrho : 0 < rho) (a : CoeffSpace d) (m : ℕ) : 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) F}

The inner spatial series defining an endpoint-relative block row is summable for every coefficient sample.

theorem HCPolySupport.HighContrast.Quenched.blockExcess_le_sub_one_of_blockMatLoewnerLE {d : ℕ} {H F : BlockMat d} (hH : IsSymmetricBlockMat H) (hHps : Matrix.PosSemidef (toFullBlockMat H)) (hF : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) {s : ℝ} (hs : 1 ≤ s) (hHF : BlockMatLoewnerLE H (blockScale s F)) : blockExcess H F ≤ s - 1

A Loewner comparison by a factor at least one bounds the normalized positive excess by that factor minus one.

theorem HCPolySupport.HighContrast.Quenched.quenched_block_row_le_of_cellExcess {d : ℕ} [NeZero d] {F : BlockMat d} (hF : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) {rho gamma D decay sourceScale : ℝ} (hgamma : 0 ≤ gamma) (hgap : gamma < rho) (hD : 0 ≤ D) (hdecay : 0 ≤ decay) (a : CoeffSpace d) (m : ℕ) (hcell : ∀ (n : ℕ) (w : Fin d → ℤ), standardCellCenter (↑m - ↑n) w ∈ centeredCube d ↑m → blockExcess (coarseBlock (standardCell d (↑m - ↑n) w) a) F ≤ D * 3 ^ (gamma * ↑n) * decay) : quenchedBlockRow rho F sourceScale a m ≤ D * decay * (1 - 3 ^ (-(rho - gamma)))⁻¹

A uniform geometric bound on every cell excess sums to the corresponding bound for the endpoint-relative block row.

theorem HCPolySupport.HighContrast.Quenched.measurable_quenched_block_row {d : ℕ} [NeZero d] {F : BlockMat d} (hF : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) {sourceScale : CoeffSpace d → ℝ} (hsource : Measurable sourceScale) {rho : ℝ} (hrho : 0 < rho) (m : ℕ) : Measurable fun (a : CoeffSpace d) => quenchedBlockRow rho F (sourceScale a) a m

The endpoint-relative block row is measurable in the coefficient sample.