Coarse-graining support: Support.Book.Ch02.Theorems.MultiscaleEllipticity.Representatives

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

Representative Bridges for Chapter 2.5 Multiscale Ellipticity

This file bridges public a.e. coefficient families to pointwise representatives used by the deterministic multiscale ellipticity estimates.

noncomputable def HCPolySupport.Book.Ch02.pointwiseCoeffOnRestrict {d : ℕ} {Q R : TriadicCube d} (aQ : CoeffOn (cubeDomain Q)) (hsub : openCubeSet R ⊆ openCubeSet Q) : CoeffOn (cubeDomain R)

Restrict the pointwise-good representative of a root-cube coefficient object to a smaller triadic cube. This is an internal bridge object: public coefficient fields remain a.e. objects, while old deterministic lemmas consume pointwise elliptic representatives.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.Book.Ch02.coeffOn_descendant_aeeq_pointwiseCoeffOnRestrict {d : ℕ} (a : TriadicCoeffFamily d) {Q R : TriadicCube d} {k : ℤ} (hk : k ≤ Q.scale) (hR : R ∈ descendantsAtScale Q k) : (a.coeffOn R).AEEq (pointwiseCoeffOnRestrict (a.coeffOn Q) ⋯)

theorem HCPolySupport.Book.Ch02.pointwiseCoeffField_openCube_descendant_data {d : ℕ} [NeZero d] (Q : TriadicCube d) (aQ : CoeffOn (cubeDomain Q)) : OpenCubeDescendantDeterministicCoarseData Q (Internal.Ch02.BookCh02.pointwiseCoeffField (cubeDomain Q) aQ)

theorem HCPolySupport.Book.Ch02.coarseBMatrixNorm_le_coarseBBlockNorm_of_mem_descendantsAtScale {d : ℕ} [NeZero d] (a : TriadicCoeffFamily d) {Q R : TriadicCube d} {k : ℤ} (hk : k ≤ Q.scale) (hR : R ∈ descendantsAtScale Q k) : coarseBMatrixNorm R a ≤ coarseBBlockNorm R (Internal.Ch02.BookCh02.pointwiseCoeffField (cubeDomain Q) (a.coeffOn Q))

theorem HCPolySupport.Book.Ch02.coarseSigmaStarInvMatrixNorm_le_coarseSigmaStarInvBlockNorm_of_mem_descendantsAtScale {d : ℕ} [NeZero d] (a : TriadicCoeffFamily d) {Q R : TriadicCube d} {k : ℤ} (hk : k ≤ Q.scale) (hR : R ∈ descendantsAtScale Q k) : coarseSigmaStarInvMatrixNorm R a ≤ coarseSigmaStarInvBlockNorm R (Internal.Ch02.BookCh02.pointwiseCoeffField (cubeDomain Q) (a.coeffOn Q))

theorem HCPolySupport.Book.Ch02.coarseBMatrixNorm_eq_matrixNorm_bCoarse_pointwiseCoeffField_of_mem_descendantsAtScale {d : ℕ} [NeZero d] (a : TriadicCoeffFamily d) {Q R : TriadicCube d} {k : ℤ} (hk : k ≤ Q.scale) (hR : R ∈ descendantsAtScale Q k) : coarseBMatrixNorm R a = matrixNorm (HCPolySupport.bCoarse (HCPolySupport.sigmaCoarse (cubeSet R) (Internal.Ch02.BookCh02.pointwiseCoeffField (cubeDomain Q) (a.coeffOn Q))) (HCPolySupport.sigmaStarCoarse (cubeSet R) (Internal.Ch02.BookCh02.pointwiseCoeffField (cubeDomain Q) (a.coeffOn Q))) (HCPolySupport.kappaCoarse (cubeSet R) (Internal.Ch02.BookCh02.pointwiseCoeffField (cubeDomain Q) (a.coeffOn Q))))

theorem HCPolySupport.Book.Ch02.coarseSigmaStarInvMatrixNorm_eq_matrixNorm_sigmaStarInv_pointwiseCoeffField {d : ℕ} [NeZero d] (a : TriadicCoeffFamily d) {Q R : TriadicCube d} {k : ℤ} (hk : k ≤ Q.scale) (hR : R ∈ descendantsAtScale Q k) : coarseSigmaStarInvMatrixNorm R a = matrixNorm (HCPolySupport.sigmaStarInvCoarse (cubeSet R) (Internal.Ch02.BookCh02.pointwiseCoeffField (cubeDomain Q) (a.coeffOn Q)))

theorem HCPolySupport.Book.Ch02.coarseBBlockNorm_le_dim_mul_coarseBMatrixNorm_of_mem_descendantsAtScale {d : ℕ} [NeZero d] (a : TriadicCoeffFamily d) {Q R : TriadicCube d} {k : ℤ} (hk : k ≤ Q.scale) (hR : R ∈ descendantsAtScale Q k) : coarseBBlockNorm R (Internal.Ch02.BookCh02.pointwiseCoeffField (cubeDomain Q) (a.coeffOn Q)) ≤ ↑d * coarseBMatrixNorm R a

theorem HCPolySupport.Book.Ch02.coarseSigmaStarInvBlockNorm_le_dim_mul_matrixNorm_on_descendant {d : ℕ} [NeZero d] (a : TriadicCoeffFamily d) {Q R : TriadicCube d} {k : ℤ} (hk : k ≤ Q.scale) (hR : R ∈ descendantsAtScale Q k) : coarseSigmaStarInvBlockNorm R (Internal.Ch02.BookCh02.pointwiseCoeffField (cubeDomain Q) (a.coeffOn Q)) ≤ ↑d * coarseSigmaStarInvMatrixNorm R a

theorem HCPolySupport.Book.Ch02.coarseBMatrixNorm_le_maxDescendantBMatrixNormAtScale {d : ℕ} [NeZero d] (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) (a : TriadicCoeffFamily d) : coarseBMatrixNorm Q a ≤ maxDescendantBMatrixNormAtScale Q k a

theorem HCPolySupport.Book.Ch02.coarseSigmaStarInvMatrixNorm_le_maxDescendantSigmaStarInvMatrixNormAtScale {d : ℕ} [NeZero d] (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) (a : TriadicCoeffFamily d) : coarseSigmaStarInvMatrixNorm Q a ≤ maxDescendantSigmaStarInvMatrixNormAtScale Q k a

theorem HCPolySupport.Book.Ch02.maxDescendantBMatrixNormAtScale_le_maxDescendantBBlockNormAtScale {d : ℕ} [NeZero d] (a : TriadicCoeffFamily d) (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) : maxDescendantBMatrixNormAtScale Q k a ≤ maxDescendantBBlockNormAtScale Q k (Internal.Ch02.BookCh02.pointwiseCoeffField (cubeDomain Q) (a.coeffOn Q))

theorem HCPolySupport.Book.Ch02.maxDescendantSigmaStarInvMatrixNormAtScale_le_maxDescendantSigmaStarInvNormAtScale {d : ℕ} [NeZero d] (a : TriadicCoeffFamily d) (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) : maxDescendantSigmaStarInvMatrixNormAtScale Q k a ≤ maxDescendantSigmaStarInvNormAtScale Q k (Internal.Ch02.BookCh02.pointwiseCoeffField (cubeDomain Q) (a.coeffOn Q))

theorem HCPolySupport.Book.Ch02.maxDescendantBBlockNormAtScale_le_dim_mul_maxDescendantBMatrixNormAtScale {d : ℕ} [NeZero d] (a : TriadicCoeffFamily d) (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) : maxDescendantBBlockNormAtScale Q k (Internal.Ch02.BookCh02.pointwiseCoeffField (cubeDomain Q) (a.coeffOn Q)) ≤ ↑d * maxDescendantBMatrixNormAtScale Q k a

theorem HCPolySupport.Book.Ch02.maxDescendantSigmaStarInvNormAtScale_le_dim_mul_maxDescendantSigmaStarInvMatrixNormAtScale {d : ℕ} [NeZero d] (a : TriadicCoeffFamily d) (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) : maxDescendantSigmaStarInvNormAtScale Q k (Internal.Ch02.BookCh02.pointwiseCoeffField (cubeDomain Q) (a.coeffOn Q)) ≤ ↑d * maxDescendantSigmaStarInvMatrixNormAtScale Q k a

theorem HCPolySupport.Book.Ch02.maxDescendantBMatrixNormAtScale_le_old_of_mem_descendantsAtScale {d : ℕ} [NeZero d] (a : TriadicCoeffFamily d) {Q R : TriadicCube d} {k l : ℤ} (hR : R ∈ descendantsAtScale Q k) (hl : l ≤ R.scale) : maxDescendantBMatrixNormAtScale R l a ≤ maxDescendantBBlockNormAtScale R l (Internal.Ch02.BookCh02.pointwiseCoeffField (cubeDomain Q) (a.coeffOn Q))

theorem HCPolySupport.Book.Ch02.maxDescendantSigmaStarInvMatrixNormAtScale_le_old_of_mem_descendantsAtScale {d : ℕ} [NeZero d] (a : TriadicCoeffFamily d) {Q R : TriadicCube d} {k l : ℤ} (hR : R ∈ descendantsAtScale Q k) (hl : l ≤ R.scale) : maxDescendantSigmaStarInvMatrixNormAtScale R l a ≤ maxDescendantSigmaStarInvNormAtScale R l (Internal.Ch02.BookCh02.pointwiseCoeffField (cubeDomain Q) (a.coeffOn Q))

theorem HCPolySupport.Book.Ch02.maxDescendantBMatrixNormAtScale_self {d : ℕ} (Q : TriadicCube d) (a : TriadicCoeffFamily d) : maxDescendantBMatrixNormAtScale Q Q.scale a = coarseBMatrixNorm Q a

theorem HCPolySupport.Book.Ch02.maxDescendantSigmaStarInvMatrixNormAtScale_self {d : ℕ} (Q : TriadicCube d) (a : TriadicCoeffFamily d) : maxDescendantSigmaStarInvMatrixNormAtScale Q Q.scale a = coarseSigmaStarInvMatrixNorm Q a

theorem HCPolySupport.Book.Ch02.maxDescendantBMatrixNormAtScale_nonneg {d : ℕ} (Q : TriadicCube d) {k : ℤ} (_hk : k ≤ Q.scale) (a : TriadicCoeffFamily d) : 0 ≤ maxDescendantBMatrixNormAtScale Q k a

theorem HCPolySupport.Book.Ch02.maxDescendantSigmaStarInvMatrixNormAtScale_nonneg {d : ℕ} (Q : TriadicCube d) {k : ℤ} (_hk : k ≤ Q.scale) (a : TriadicCoeffFamily d) : 0 ≤ maxDescendantSigmaStarInvMatrixNormAtScale Q k a

theorem HCPolySupport.Book.Ch02.maxDescendantBMatrixNormAtScale_le_of_mem_descendantsAtScale {d : ℕ} (a : TriadicCoeffFamily d) {Q R : TriadicCube d} {k l : ℤ} (hR : R ∈ descendantsAtScale Q k) (hl : l ≤ R.scale) : maxDescendantBMatrixNormAtScale R l a ≤ maxDescendantBMatrixNormAtScale Q l a

theorem HCPolySupport.Book.Ch02.maxDescendantSigmaStarInvMatrixNormAtScale_le_of_mem_descendantsAtScale {d : ℕ} (a : TriadicCoeffFamily d) {Q R : TriadicCube d} {k l : ℤ} (hR : R ∈ descendantsAtScale Q k) (hl : l ≤ R.scale) : maxDescendantSigmaStarInvMatrixNormAtScale R l a ≤ maxDescendantSigmaStarInvMatrixNormAtScale Q l a

theorem HCPolySupport.Book.Ch02.maxDescendantBMatrixNormAtScale_le_of_le {d : ℕ} [NeZero d] (a : TriadicCoeffFamily d) (Q : TriadicCube d) {l k : ℤ} (hlk : l ≤ k) (hk : k ≤ Q.scale) : maxDescendantBMatrixNormAtScale Q k a ≤ maxDescendantBMatrixNormAtScale Q l a

theorem HCPolySupport.Book.Ch02.maxDescendantSigmaStarInvMatrixNormAtScale_le_of_le {d : ℕ} [NeZero d] (a : TriadicCoeffFamily d) (Q : TriadicCube d) {l k : ℤ} (hlk : l ≤ k) (hk : k ≤ Q.scale) : maxDescendantSigmaStarInvMatrixNormAtScale Q k a ≤ maxDescendantSigmaStarInvMatrixNormAtScale Q l a

theorem HCPolySupport.Book.Ch02.summable_old_B_series_pointwiseCoeffField {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {s q : ℝ} (hs : 0 < s) (hq : 0 < q) : Summable fun (n : ℕ) => HCPolySupport.geometricWeight s q n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) (Internal.Ch02.BookCh02.pointwiseCoeffField (cubeDomain Q) (a.coeffOn Q))).rpow (q / 2)

theorem HCPolySupport.Book.Ch02.summable_old_sigmaStarInv_series_pointwiseCoeffField {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {s q : ℝ} (hs : 0 < s) (hq : 0 < q) : Summable fun (n : ℕ) => HCPolySupport.geometricWeight s q n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) (Internal.Ch02.BookCh02.pointwiseCoeffField (cubeDomain Q) (a.coeffOn Q))).rpow (q / 2)

theorem HCPolySupport.Book.Ch02.summable_B_series_pointwiseCoeffField {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {s q : ℝ} (hs : 0 < s) (hq : 0 < q) : Summable fun (n : ℕ) => geometricWeight s q n * (maxDescendantBMatrixNormAtScale Q (Q.scale - ↑n) a).rpow (q / 2)

theorem HCPolySupport.Book.Ch02.summable_sigmaStarInv_series_pointwiseCoeffField {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {s q : ℝ} (hs : 0 < s) (hq : 0 < q) : Summable fun (n : ℕ) => geometricWeight s q n * (maxDescendantSigmaStarInvMatrixNormAtScale Q (Q.scale - ↑n) a).rpow (q / 2)