Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch02.Theorems.MultiscaleEllipticity.Public

Coarse-graining support: Support.Book.Ch02.Theorems.MultiscaleEllipticity.Public #

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

Public Chapter 2.5 Multiscale Ellipticity Theorems #

This file assembles the public theorem packages and records that the multiscale ellipticity quantities depend only on a.e. coefficient data.

source
theorem HCPolySupport.Book.Ch02.multiscaleEllipticityBasicTheory {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) :
MultiscaleEllipticityBasicTheory Q a

Public theorem package for the Sec. 2.5 basic order and localization facts.

source
theorem HCPolySupport.Book.Ch02.coarseBMatrixNorm_eq_ofAEEq {d : ℕ} {a b : TriadicCoeffFamily d} (h : a.AEEq b) (Q : TriadicCube d) :
coarseBMatrixNorm Q a = coarseBMatrixNorm Q b
source
theorem HCPolySupport.Book.Ch02.coarseSigmaStarInvMatrixNorm_eq_ofAEEq {d : ℕ} {a b : TriadicCoeffFamily d} (h : a.AEEq b) (Q : TriadicCube d) :
coarseSigmaStarInvMatrixNorm Q a = coarseSigmaStarInvMatrixNorm Q b
source
theorem HCPolySupport.Book.Ch02.maxDescendantBMatrixNormAtScale_eq_ofAEEq {d : ℕ} {a b : TriadicCoeffFamily d} (h : a.AEEq b) (Q : TriadicCube d) (k : ℤ) :
maxDescendantBMatrixNormAtScale Q k a = maxDescendantBMatrixNormAtScale Q k b
source
theorem HCPolySupport.Book.Ch02.maxDescendantSigmaStarInvMatrixNormAtScale_eq_ofAEEq {d : ℕ} {a b : TriadicCoeffFamily d} (h : a.AEEq b) (Q : TriadicCube d) (k : ℤ) :
maxDescendantSigmaStarInvMatrixNormAtScale Q k a = maxDescendantSigmaStarInvMatrixNormAtScale Q k b
source
theorem HCPolySupport.Book.Ch02.maxDescendantBMatrixNormAtScale_translateCube_of_coarseBMatrixNorm {d : ℕ} (a b : TriadicCoeffFamily d) (z : Fin d → ℤ) (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) (hB : ∀ R ∈ descendantsAtScale Q k, coarseBMatrixNorm (translateCube (descendantTranslationShift (Q.scale - k).toNat z) R) a = coarseBMatrixNorm R b) :
maxDescendantBMatrixNormAtScale (translateCube z Q) k a = maxDescendantBMatrixNormAtScale Q k b
source
theorem HCPolySupport.Book.Ch02.maxDescendantSigmaStarInvMatrixNormAtScale_translateCube_of_coarseSigmaStarInvMatrixNorm {d : ℕ} (a b : TriadicCoeffFamily d) (z : Fin d → ℤ) (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) (hSigma : ∀ R ∈ descendantsAtScale Q k, coarseSigmaStarInvMatrixNorm (translateCube (descendantTranslationShift (Q.scale - k).toNat z) R) a = coarseSigmaStarInvMatrixNorm R b) :
maxDescendantSigmaStarInvMatrixNormAtScale (translateCube z Q) k a = maxDescendantSigmaStarInvMatrixNormAtScale Q k b
source
theorem HCPolySupport.Book.Ch02.LambdaSqFinite_translateCube_of_coarseBMatrixNorm {d : ℕ} (a b : TriadicCoeffFamily d) (z : Fin d → ℤ) (Q : TriadicCube d) (s q : ℝ) (hB : ∀ (n : ℕ), ∀ R ∈ descendantsAtScale Q (Q.scale - ↑n), coarseBMatrixNorm (translateCube (descendantTranslationShift n z) R) a = coarseBMatrixNorm R b) :
LambdaSqFinite (translateCube z Q) s q a = LambdaSqFinite Q s q b
source
theorem HCPolySupport.Book.Ch02.lambdaSqFinite_translateCube_of_coarseSigmaStarInvMatrixNorm {d : ℕ} (a b : TriadicCoeffFamily d) (z : Fin d → ℤ) (Q : TriadicCube d) (s q : ℝ) (hSigma : ∀ (n : ℕ), ∀ R ∈ descendantsAtScale Q (Q.scale - ↑n), coarseSigmaStarInvMatrixNorm (translateCube (descendantTranslationShift n z) R) a = coarseSigmaStarInvMatrixNorm R b) :
lambdaSqFinite (translateCube z Q) s q a = lambdaSqFinite Q s q b
source
theorem HCPolySupport.Book.Ch02.LambdaSqInfinity_translateCube_of_coarseBMatrixNorm {d : ℕ} (a b : TriadicCoeffFamily d) (z : Fin d → ℤ) (Q : TriadicCube d) (s : ℝ) (hB : ∀ (n : ℕ), ∀ R ∈ descendantsAtScale Q (Q.scale - ↑n), coarseBMatrixNorm (translateCube (descendantTranslationShift n z) R) a = coarseBMatrixNorm R b) :
LambdaSqInfinity (translateCube z Q) s a = LambdaSqInfinity Q s b
source
theorem HCPolySupport.Book.Ch02.lambdaSqInfinity_translateCube_of_coarseSigmaStarInvMatrixNorm {d : ℕ} (a b : TriadicCoeffFamily d) (z : Fin d → ℤ) (Q : TriadicCube d) (s : ℝ) (hSigma : ∀ (n : ℕ), ∀ R ∈ descendantsAtScale Q (Q.scale - ↑n), coarseSigmaStarInvMatrixNorm (translateCube (descendantTranslationShift n z) R) a = coarseSigmaStarInvMatrixNorm R b) :
lambdaSqInfinity (translateCube z Q) s a = lambdaSqInfinity Q s b
source
theorem HCPolySupport.Book.Ch02.LambdaSq_translateCube_of_coarseBMatrixNorm {d : ℕ} (a b : TriadicCoeffFamily d) (z : Fin d → ℤ) (Q : TriadicCube d) (s : ℝ) (q : MultiscaleExponent) (hB : ∀ (n : ℕ), ∀ R ∈ descendantsAtScale Q (Q.scale - ↑n), coarseBMatrixNorm (translateCube (descendantTranslationShift n z) R) a = coarseBMatrixNorm R b) :
LambdaSq (translateCube z Q) s q a = LambdaSq Q s q b
source
theorem HCPolySupport.Book.Ch02.lambdaSq_translateCube_of_coarseSigmaStarInvMatrixNorm {d : ℕ} (a b : TriadicCoeffFamily d) (z : Fin d → ℤ) (Q : TriadicCube d) (s : ℝ) (q : MultiscaleExponent) (hSigma : ∀ (n : ℕ), ∀ R ∈ descendantsAtScale Q (Q.scale - ↑n), coarseSigmaStarInvMatrixNorm (translateCube (descendantTranslationShift n z) R) a = coarseSigmaStarInvMatrixNorm R b) :
lambdaSq (translateCube z Q) s q a = lambdaSq Q s q b
source
theorem HCPolySupport.Book.Ch02.LambdaSqFinite_eq_ofAEEq {d : ℕ} {a b : TriadicCoeffFamily d} (h : a.AEEq b) (Q : TriadicCube d) (s q : ℝ) :
LambdaSqFinite Q s q a = LambdaSqFinite Q s q b
source
theorem HCPolySupport.Book.Ch02.lambdaSqFinite_eq_ofAEEq {d : ℕ} {a b : TriadicCoeffFamily d} (h : a.AEEq b) (Q : TriadicCube d) (s q : ℝ) :
lambdaSqFinite Q s q a = lambdaSqFinite Q s q b
source
theorem HCPolySupport.Book.Ch02.LambdaSqInfinity_eq_ofAEEq {d : ℕ} {a b : TriadicCoeffFamily d} (h : a.AEEq b) (Q : TriadicCube d) (s : ℝ) :
LambdaSqInfinity Q s a = LambdaSqInfinity Q s b
source
theorem HCPolySupport.Book.Ch02.lambdaSqInfinity_eq_ofAEEq {d : ℕ} {a b : TriadicCoeffFamily d} (h : a.AEEq b) (Q : TriadicCube d) (s : ℝ) :
lambdaSqInfinity Q s a = lambdaSqInfinity Q s b
source
theorem HCPolySupport.Book.Ch02.LambdaSq_eq_ofAEEq {d : ℕ} {a b : TriadicCoeffFamily d} (h : a.AEEq b) (Q : TriadicCube d) (s : ℝ) (q : MultiscaleExponent) :
LambdaSq Q s q a = LambdaSq Q s q b
source
theorem HCPolySupport.Book.Ch02.lambdaSq_eq_ofAEEq {d : ℕ} {a b : TriadicCoeffFamily d} (h : a.AEEq b) (Q : TriadicCube d) (s : ℝ) (q : MultiscaleExponent) :
lambdaSq Q s q a = lambdaSq Q s q b
source
theorem HCPolySupport.Book.Ch02.LambdaS_eq_ofAEEq {d : ℕ} {a b : TriadicCoeffFamily d} (h : a.AEEq b) (Q : TriadicCube d) (s : ℝ) :
LambdaS Q s a = LambdaS Q s b
source
theorem HCPolySupport.Book.Ch02.lambdaS_eq_ofAEEq {d : ℕ} {a b : TriadicCoeffFamily d} (h : a.AEEq b) (Q : TriadicCube d) (s : ℝ) :
lambdaS Q s a = lambdaS Q s b
source
theorem HCPolySupport.Book.Ch02.ThetaRatio_eq_ofAEEq {d : ℕ} {a b : TriadicCoeffFamily d} (h : a.AEEq b) (Q : TriadicCube d) (s t : ℝ) :
ThetaRatio Q s t a = ThetaRatio Q s t b
source
theorem HCPolySupport.Book.Ch02.multiscaleEllipticityAEEqTheory (d : ℕ) :
MultiscaleEllipticityAEEqTheory d

Public theorem package asserting that Sec. 2.5 quantities depend only on the coefficient family modulo a.e. equality on each triadic cube.

source
theorem HCPolySupport.Book.Ch02.multiscaleEllipticityChangeExponentTheory (d : ℕ) [NeZero d] :
MultiscaleEllipticityChangeExponentTheory d
source
theorem HCPolySupport.Book.Ch02.multiscaleEllipticityTheory (d : ℕ) [NeZero d] :
MultiscaleEllipticityTheory d