Coarse-graining support: Support.Book.Ch05.Theorems.Section57.NormalizedResponseEllipticity

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

Normalized response from coarse ellipticity

This file supplies the deterministic estimate used to control negative-scale sampled responses in the finite-q homogenization-error corollary. The estimate is pointwise and contains no stochastic input.

theorem HCPolySupport.Book.Ch05.Section57.blockVecDot_scalarConstantNormalizers_eq_fullBlockVecNormSq {d : ℕ} {σ : ℝ} (hσ : 0 < σ) (e : FullBlockVec d) : blockVecDot (ofFullBlockVec (Matrix.mulVec (Ch02.constantFullBlockMatrixInvSqrt (scalarMatrix σ)) e)) (ofFullBlockVec (Matrix.mulVec (Ch02.constantFullBlockMatrixSqrt (scalarMatrix σ)) e)) = Ch02.fullBlockVecNormSq e

The two scalar normalizers used in the normalized response are dual.

theorem HCPolySupport.Book.Ch05.Section57.normalizedBlockResponseMax_scalarMatrix_le_weightedCoarseEllipticity {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : Ch02.TriadicCoeffFamily d) {σ : ℝ} (hσ : 0 < σ) : Ch02.normalizedBlockResponseMax Q a (scalarMatrix σ) ≤ ↑(Fintype.card (BlockCoord d)) ^ 2 * (σ⁻¹ * Ch02.coarseBMatrixNorm Q a + σ * Ch02.coarseSigmaStarInvMatrixNorm Q a)

One-cube normalized response is bounded by the scalar-weighted coarse ellipticity of that cube.

theorem HCPolySupport.Book.Ch05.Section57.maxDescendantNormalizedBlockResponseAtScale_scalarMatrix_le_weightedEllipticity {d : ℕ} [NeZero d] (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) (a : Ch02.TriadicCoeffFamily d) {σ : ℝ} (hσ : 0 < σ) : Ch02.maxDescendantNormalizedBlockResponseAtScale Q k a (scalarMatrix σ) ≤ ↑(Fintype.card (BlockCoord d)) ^ 2 * (σ⁻¹ * Ch02.maxDescendantBMatrixNormAtScale Q k a + σ * Ch02.maxDescendantSigmaStarInvMatrixNormAtScale Q k a)

Descendant-scale normalized response is bounded by the corresponding weighted descendant ellipticity maxima.

theorem HCPolySupport.Book.Ch05.Section57.scaleResponseAtScale_scalarMatrix_le_sqrt_weightedEllipticity {d : ℕ} [NeZero d] (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) (a : Ch02.TriadicCoeffFamily d) {σ : ℝ} (hσ : 0 < σ) : Ch02.scaleResponseAtScale Q k Ch02.MultiscaleExponent.infinity a (scalarMatrix σ) ≤ √(↑(Fintype.card (BlockCoord d)) ^ 2 * (σ⁻¹ * Ch02.maxDescendantBMatrixNormAtScale Q k a + σ * Ch02.maxDescendantSigmaStarInvMatrixNormAtScale Q k a))

Square-root scale-response form of maxDescendantNormalizedBlockResponseAtScale_scalarMatrix_le_weightedEllipticity.

theorem HCPolySupport.Book.Ch05.Section57.weighted_scaleResponseAtScale_originCube_neg_nat_scalarMatrix_le_ellipticityRows {d : ℕ} [NeZero d] (m j : ℕ) {s σ : ℝ} (hs : 0 ≤ s) (hσ : 0 < σ) (a : Ch02.TriadicCoeffFamily d) : Ch02.geometricWeight s 1 (j + m) * Ch02.scaleResponseAtScale (originCube d ↑m) (-↑j) Ch02.MultiscaleExponent.infinity a (scalarMatrix σ) ≤ √(↑(Fintype.card (BlockCoord d)) ^ 2) * (√σ⁻¹ * (Ch02.geometricWeight s 1 (j + m) * (Ch02.maxDescendantBMatrixNormAtScale (originCube d ↑m) (-↑j) a).rpow (1 / 2)) + √σ * (Ch02.geometricWeight s 1 (j + m) * (Ch02.maxDescendantSigmaStarInvMatrixNormAtScale (originCube d ↑m) (-↑j) a).rpow (1 / 2)))

One negative-scale row of the scalar-normalized response is controlled by the two Ch2 unit-ellipticity square-root rows.