Coarse-graining support: Support.Book.Ch02.Theorems.HomogenizationError.EllipticityControl

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

Ellipticity control by the homogenization error

This file starts the Ch2 bridge from the normalized homogenization error \mathcal E to the coarse-grained ellipticity factors. The first endpoint needed downstream is the finite q = 2, scalar-normalized estimate.

theorem HCPolySupport.Book.Ch02.constantFullBlockMatrix_posDef_of_isEllipticMatrix {d : ℕ} {lam Lam : ℝ} {a0 : Mat d} (ha0 : IsEllipticMatrix lam Lam a0) : Matrix.PosDef (constantFullBlockMatrix a0)

theorem HCPolySupport.Book.Ch02.constantFullBlockMatrixSqrt_isSymm {d : ℕ} (a0 : Mat d) : Matrix.IsSymm (constantFullBlockMatrixSqrt a0)

theorem HCPolySupport.Book.Ch02.fullBlockVecNormSq_constantFullBlockMatrixSqrt_mul_toFullBlockVec_eq {d : ℕ} {a0 : Mat d} {lam Lam : ℝ} (ha0 : IsEllipticMatrix lam Lam a0) (P : BlockVec d) : fullBlockVecNormSq (Matrix.mulVec (constantFullBlockMatrixSqrt a0) (toFullBlockVec P)) = blockVecDot P (blockMatVecMul (constantBlockMatrix a0) P)

theorem HCPolySupport.Book.Ch02.normalizedBlockResponseValueSet_mem_of_constantBlockQuadratic_eq_one {d : ℕ} (Q : TriadicCube d) (a : TriadicCoeffFamily d) {a0 : Mat d} {lam Lam : ℝ} (ha0 : IsEllipticMatrix lam Lam a0) (P : BlockVec d) (hquad : blockVecDot P (blockMatVecMul (constantBlockMatrix a0) P) = 1) : doubledResponseJ (cubeDomain Q) (a.coeffOn Q) P (blockMatVecMul (constantBlockMatrix a0) P) ∈ normalizedBlockResponseValueSet Q a a0

theorem HCPolySupport.Book.Ch02.matrixNorm_le_trace_of_posSemidef {d : ℕ} (M : Mat d) (hM : Matrix.PosSemidef M) : matrixNorm M ≤ Matrix.trace M

theorem HCPolySupport.Book.Ch02.matTranspose_scalarMatrix {d : ℕ} (σ : ℝ) : matTranspose (scalarMatrix σ) = scalarMatrix σ

theorem HCPolySupport.Book.Ch02.symmPart_scalarMatrix {d : ℕ} (σ : ℝ) : symmPart (scalarMatrix σ) = scalarMatrix σ

theorem HCPolySupport.Book.Ch02.skewPart_scalarMatrix {d : ℕ} (σ : ℝ) : skewPart (scalarMatrix σ) = 0

theorem HCPolySupport.Book.Ch02.constantBlockMatrix_scalarMatrix {d : ℕ} {σ : ℝ} (hσ : 0 < σ) : constantBlockMatrix (scalarMatrix σ) = { upperLeft := scalarMatrix σ, upperRight := 0, lowerLeft := 0, lowerRight := scalarMatrix σ⁻¹ }

theorem HCPolySupport.Book.Ch02.doubledResponseJ_scalarCoordinateProbe_le_normalizedBlockResponseMax {d : ℕ} (Q : TriadicCube d) (a : TriadicCoeffFamily d) {σ : ℝ} (hσ : 0 < σ) (i : Fin d) : doubledResponseJ (cubeDomain Q) (a.coeffOn Q) ((√σ)⁻¹ • Pi.single i 1, 0) (√σ • Pi.single i 1, 0) ≤ normalizedBlockResponseMax Q a (scalarMatrix σ)

theorem HCPolySupport.Book.Ch02.specialCoordinateBlockJTraceBudget_le_card_mul_normalizedBlockResponseMax {d : ℕ} (Q : TriadicCube d) (a : TriadicCoeffFamily d) {σ : ℝ} (hσ : 0 < σ) : specialCoordinateBlockJTraceBudget σ (coarseBlockMatrix (cubeDomain Q) (a.coeffOn Q)) ≤ ↑(Fintype.card (Fin d)) * normalizedBlockResponseMax Q a (scalarMatrix σ)

theorem HCPolySupport.Book.Ch02.weightedTrace_coarseBlockMatrix_eq_two_mul_budget_add_card {d : ℕ} (U : Domain d) (a : CoeffOn U) (σ : ℝ) : σ⁻¹ * Matrix.trace (bCoarse U a) + σ * Matrix.trace (sigmaStarInvCoarse U a) = 2 * (specialCoordinateBlockJTraceBudget σ (coarseBlockMatrix U a) + ↑(Fintype.card (Fin d)))

theorem HCPolySupport.Book.Ch02.weightedCoarseEllipticityNorm_le_card_mul_normalizedBlockResponseMax_add_one {d : ℕ} (Q : TriadicCube d) (a : TriadicCoeffFamily d) {σ : ℝ} (hσ : 0 < σ) : σ⁻¹ * coarseBMatrixNorm Q a + σ * coarseSigmaStarInvMatrixNorm Q a ≤ 2 * ↑(Fintype.card (Fin d)) * (normalizedBlockResponseMax Q a (scalarMatrix σ) + 1)

theorem HCPolySupport.Book.Ch02.inv_mul_coarseBMatrixNorm_le_card_mul_normalizedBlockResponseMax_add_one {d : ℕ} (Q : TriadicCube d) (a : TriadicCoeffFamily d) {σ : ℝ} (hσ : 0 < σ) : σ⁻¹ * coarseBMatrixNorm Q a ≤ 2 * ↑(Fintype.card (Fin d)) * (normalizedBlockResponseMax Q a (scalarMatrix σ) + 1)

theorem HCPolySupport.Book.Ch02.sigma_mul_coarseSigmaStarInvMatrixNorm_le_card_mul_normalizedBlockResponseMax_add_one {d : ℕ} (Q : TriadicCube d) (a : TriadicCoeffFamily d) {σ : ℝ} (hσ : 0 < σ) : σ * coarseSigmaStarInvMatrixNorm Q a ≤ 2 * ↑(Fintype.card (Fin d)) * (normalizedBlockResponseMax Q a (scalarMatrix σ) + 1)

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

theorem HCPolySupport.Book.Ch02.sigma_mul_maxDescendantSigmaStarInvMatrixNormAtScale_le_card_mul_maxResponse_add_one {d : ℕ} [NeZero d] (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) (a : TriadicCoeffFamily d) {σ : ℝ} (hσ : 0 < σ) : σ * maxDescendantSigmaStarInvMatrixNormAtScale Q k a ≤ 2 * ↑(Fintype.card (Fin d)) * (maxDescendantNormalizedBlockResponseAtScale Q k a (scalarMatrix σ) + 1)

theorem HCPolySupport.Book.Ch02.summable_geometricWeight_two_mul_maxDescendantNormalizedBlockResponseAtScale {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) (a0 : Mat d) {s : ℝ} (hs : 0 < s) : Summable fun (n : ℕ) => geometricWeight s 2 n * maxDescendantNormalizedBlockResponseAtScale Q (Q.scale - ↑n) a a0

theorem HCPolySupport.Book.Ch02.tsum_geometricWeight_two_mul_maxResponse_add_one_eq_homogenizationError_sq_add_one {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) (a0 : Mat d) {s : ℝ} (hs : 0 < s) : ∑' (n : ℕ), geometricWeight s 2 n * (maxDescendantNormalizedBlockResponseAtScale Q (Q.scale - ↑n) a a0 + 1) = HomogenizationErrorOnCube Q s MultiscaleExponent.infinity (MultiscaleExponent.finite 2) a a0 ^ 2 + 1

theorem HCPolySupport.Book.Ch02.inv_mul_LambdaSq_finite_two_le_card_mul_homogenizationError_sq_add_one {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {s σ : ℝ} (hs : 0 < s) (hσ : 0 < σ) : σ⁻¹ * LambdaSq Q s (MultiscaleExponent.finite 2) a ≤ 2 * ↑(Fintype.card (Fin d)) * (HomogenizationErrorOnCube Q s MultiscaleExponent.infinity (MultiscaleExponent.finite 2) a (scalarMatrix σ) ^ 2 + 1)

theorem HCPolySupport.Book.Ch02.sigma_mul_lambdaSq_finite_two_inv_le_card_mul_homogenizationError_sq_add_one {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {s σ : ℝ} (hs : 0 < s) (hσ : 0 < σ) : σ * (lambdaSq Q s (MultiscaleExponent.finite 2) a)⁻¹ ≤ 2 * ↑(Fintype.card (Fin d)) * (HomogenizationErrorOnCube Q s MultiscaleExponent.infinity (MultiscaleExponent.finite 2) a (scalarMatrix σ) ^ 2 + 1)

theorem HCPolySupport.Book.Ch02.max_weightedEllipticity_finite_two_le_card_mul_homogenizationError_sq_add_one {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {s σ : ℝ} (hs : 0 < s) (hσ : 0 < σ) : max (σ⁻¹ * LambdaSq Q s (MultiscaleExponent.finite 2) a) (σ * (lambdaSq Q s (MultiscaleExponent.finite 2) a)⁻¹) ≤ 2 * ↑(Fintype.card (Fin d)) * (HomogenizationErrorOnCube Q s MultiscaleExponent.infinity (MultiscaleExponent.finite 2) a (scalarMatrix σ) ^ 2 + 1)

theorem HCPolySupport.Book.Ch02.weightedEllipticity_finite_two_le_card_mul_homogenizationError_sq_add_one {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {s σ : ℝ} (hs : 0 < s) (hσ : 0 < σ) : σ⁻¹ * LambdaSq Q s (MultiscaleExponent.finite 2) a + σ * (lambdaSq Q s (MultiscaleExponent.finite 2) a)⁻¹ ≤ 4 * ↑(Fintype.card (Fin d)) * (HomogenizationErrorOnCube Q s MultiscaleExponent.infinity (MultiscaleExponent.finite 2) a (scalarMatrix σ) ^ 2 + 1)