Documentation

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

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

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

Localization for Chapter 2.5 Multiscale Ellipticity #

This file proves descendant localization bounds and the unified finite/infinite public order lemmas, including the theta-ratio controls.

source
theorem HCPolySupport.Book.Ch02.descendant_LambdaSq_infinity_le {d : ℕ} [NeZero d] {Q R : TriadicCube d} {k : ℤ} (a : TriadicCoeffFamily d) {s : ℝ} (hR : R ∈ descendantsAtScale Q k) (hs : 0 < s) :
LambdaSq R s MultiscaleExponent.infinity a ≤ multiscaleDescendantWeight Q k s * LambdaSq Q s MultiscaleExponent.infinity a
source
theorem HCPolySupport.Book.Ch02.descendant_lambdaSq_infinity_inv_le {d : ℕ} [NeZero d] {Q R : TriadicCube d} {k : ℤ} (a : TriadicCoeffFamily d) {s : ℝ} (hR : R ∈ descendantsAtScale Q k) (hs : 0 < s) :
(lambdaSq R s MultiscaleExponent.infinity a)⁻¹ ≤ multiscaleDescendantWeight Q k s * (lambdaSq Q s MultiscaleExponent.infinity a)⁻¹
source
theorem HCPolySupport.Book.Ch02.descendant_LambdaSq_finite_le {d : ℕ} [NeZero d] {Q R : TriadicCube d} {k : ℤ} (a : TriadicCoeffFamily d) {s q : ℝ} (hR : R ∈ descendantsAtScale Q k) (hs : 0 < s) (hq : 1 ≤ q) :
LambdaSq R s (MultiscaleExponent.finite q) a ≤ multiscaleDescendantWeight Q k s * LambdaSq Q s (MultiscaleExponent.finite q) a
source
theorem HCPolySupport.Book.Ch02.descendant_lambdaSq_finite_inv_le {d : ℕ} [NeZero d] {Q R : TriadicCube d} {k : ℤ} (a : TriadicCoeffFamily d) {s q : ℝ} (hR : R ∈ descendantsAtScale Q k) (hs : 0 < s) (hq : 1 ≤ q) :
(lambdaSq R s (MultiscaleExponent.finite q) a)⁻¹ ≤ multiscaleDescendantWeight Q k s * (lambdaSq Q s (MultiscaleExponent.finite q) a)⁻¹
source
theorem HCPolySupport.Book.Ch02.maxDescendant_b_le_maxDescendant_LambdaSq_finite {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {k : ℤ} {s q : ℝ} (hk : k ≤ Q.scale) (hs : 0 < s) (hq : 1 ≤ q) :
maxDescendantBMatrixNormAtScale Q k a ≤ maxDescendantUpperEllipticityAtScale Q k s (MultiscaleExponent.finite q) a
source
theorem HCPolySupport.Book.Ch02.maxDescendant_sigmaStarInv_le_maxDescendant_lambdaSq_finite_inv {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {k : ℤ} {s q : ℝ} (hk : k ≤ Q.scale) (hs : 0 < s) (hq : 1 ≤ q) :
maxDescendantSigmaStarInvMatrixNormAtScale Q k a ≤ maxDescendantLowerEllipticityInvAtScale Q k s (MultiscaleExponent.finite q) a
source
theorem HCPolySupport.Book.Ch02.maxDescendant_LambdaSq_finite_le {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {k : ℤ} {s q : ℝ} (hk : k ≤ Q.scale) (hs : 0 < s) (hq : 1 ≤ q) :
maxDescendantUpperEllipticityAtScale Q k s (MultiscaleExponent.finite q) a ≤ multiscaleDescendantWeight Q k s * LambdaSq Q s (MultiscaleExponent.finite q) a
source
theorem HCPolySupport.Book.Ch02.maxDescendant_lambdaSq_finite_inv_le {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {k : ℤ} {s q : ℝ} (hk : k ≤ Q.scale) (hs : 0 < s) (hq : 1 ≤ q) :
maxDescendantLowerEllipticityInvAtScale Q k s (MultiscaleExponent.finite q) a ≤ multiscaleDescendantWeight Q k s * (lambdaSq Q s (MultiscaleExponent.finite q) a)⁻¹
source
theorem HCPolySupport.Book.Ch02.maxDescendant_b_le_maxDescendant_LambdaSq_infinity {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {k : ℤ} {s : ℝ} (hk : k ≤ Q.scale) (hs : 0 < s) :
maxDescendantBMatrixNormAtScale Q k a ≤ maxDescendantUpperEllipticityAtScale Q k s MultiscaleExponent.infinity a
source
theorem HCPolySupport.Book.Ch02.maxDescendant_sigmaStarInv_le_maxDescendant_lambdaSq_infinity_inv {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {k : ℤ} {s : ℝ} (hk : k ≤ Q.scale) (hs : 0 < s) :
maxDescendantSigmaStarInvMatrixNormAtScale Q k a ≤ maxDescendantLowerEllipticityInvAtScale Q k s MultiscaleExponent.infinity a
source
theorem HCPolySupport.Book.Ch02.maxDescendant_LambdaSq_infinity_le {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {k : ℤ} {s : ℝ} (hk : k ≤ Q.scale) (hs : 0 < s) :
maxDescendantUpperEllipticityAtScale Q k s MultiscaleExponent.infinity a ≤ multiscaleDescendantWeight Q k s * LambdaSq Q s MultiscaleExponent.infinity a
source
theorem HCPolySupport.Book.Ch02.maxDescendant_lambdaSq_infinity_inv_le {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {k : ℤ} {s : ℝ} (hk : k ≤ Q.scale) (hs : 0 < s) :
maxDescendantLowerEllipticityInvAtScale Q k s MultiscaleExponent.infinity a ≤ multiscaleDescendantWeight Q k s * (lambdaSq Q s MultiscaleExponent.infinity a)⁻¹
source
theorem HCPolySupport.Book.Ch02.LambdaSq_nonneg {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {s : ℝ} {q : MultiscaleExponent} (hs : 0 < s) (hq : q.IsAdmissible) :
0 ≤ LambdaSq Q s q a
source
theorem HCPolySupport.Book.Ch02.lambdaSq_nonneg {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {s : ℝ} {q : MultiscaleExponent} (hs : 0 < s) (hq : q.IsAdmissible) :
0 ≤ lambdaSq Q s q a
source
theorem HCPolySupport.Book.Ch02.LambdaSq_pos {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {s : ℝ} {q : MultiscaleExponent} (hs : 0 < s) (hq : q.IsAdmissible) :
0 < LambdaSq Q s q a
source
theorem HCPolySupport.Book.Ch02.lambdaSq_pos {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {s : ℝ} {q : MultiscaleExponent} (hs : 0 < s) (hq : q.IsAdmissible) :
0 < lambdaSq Q s q a
source
theorem HCPolySupport.Book.Ch02.lambdaSq_mono {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {t s : ℝ} {q : MultiscaleExponent} (ht : 0 < t) (hts : t < s) (hq : q.IsAdmissible) :
lambdaSq Q t q a ≤ lambdaSq Q s q a
source
theorem HCPolySupport.Book.Ch02.LambdaSq_antitone {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {t s : ℝ} {q : MultiscaleExponent} (ht : 0 < t) (hts : t < s) (hq : q.IsAdmissible) :
LambdaSq Q s q a ≤ LambdaSq Q t q a
source
theorem HCPolySupport.Book.Ch02.lambdaSq_le_oneCube {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {s : ℝ} {q : MultiscaleExponent} (hs : 0 < s) (hq : q.IsAdmissible) :
lambdaSq Q s q a ≤ (coarseSigmaStarInvMatrixNorm Q a)⁻¹
source
theorem HCPolySupport.Book.Ch02.oneCube_b_le_LambdaSq {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {s : ℝ} {q : MultiscaleExponent} (hs : 0 < s) (hq : q.IsAdmissible) :
coarseBMatrixNorm Q a ≤ LambdaSq Q s q a
source
theorem HCPolySupport.Book.Ch02.maxDescendant_b_le_maxDescendant_LambdaSq {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {k : ℤ} {s : ℝ} {q : MultiscaleExponent} (hk : k ≤ Q.scale) (hs : 0 < s) (hq : q.IsAdmissible) :
maxDescendantBMatrixNormAtScale Q k a ≤ maxDescendantUpperEllipticityAtScale Q k s q a
source
theorem HCPolySupport.Book.Ch02.maxDescendant_sigmaStarInv_le_maxDescendant_lambdaSq_inv {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {k : ℤ} {s : ℝ} {q : MultiscaleExponent} (hk : k ≤ Q.scale) (hs : 0 < s) (hq : q.IsAdmissible) :
maxDescendantSigmaStarInvMatrixNormAtScale Q k a ≤ maxDescendantLowerEllipticityInvAtScale Q k s q a
source
theorem HCPolySupport.Book.Ch02.maxDescendant_LambdaSq_le {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {k : ℤ} {s : ℝ} {q : MultiscaleExponent} (hk : k ≤ Q.scale) (hs : 0 < s) (hq : q.IsAdmissible) :
maxDescendantUpperEllipticityAtScale Q k s q a ≤ multiscaleDescendantWeight Q k s * LambdaSq Q s q a
source
theorem HCPolySupport.Book.Ch02.maxDescendant_lambdaSq_inv_le {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {k : ℤ} {s : ℝ} {q : MultiscaleExponent} (hk : k ≤ Q.scale) (hs : 0 < s) (hq : q.IsAdmissible) :
maxDescendantLowerEllipticityInvAtScale Q k s q a ≤ multiscaleDescendantWeight Q k s * (lambdaSq Q s q a)⁻¹
source
theorem HCPolySupport.Book.Ch02.descendant_LambdaSq_le {d : ℕ} [NeZero d] {Q R : TriadicCube d} {k : ℤ} (a : TriadicCoeffFamily d) {s : ℝ} {q : MultiscaleExponent} (hR : R ∈ descendantsAtScale Q k) (hs : 0 < s) (hq : q.IsAdmissible) :
LambdaSq R s q a ≤ multiscaleDescendantWeight Q k s * LambdaSq Q s q a
source
theorem HCPolySupport.Book.Ch02.descendant_lambdaSq_inv_le {d : ℕ} [NeZero d] {Q R : TriadicCube d} {k : ℤ} (a : TriadicCoeffFamily d) {s : ℝ} {q : MultiscaleExponent} (hR : R ∈ descendantsAtScale Q k) (hs : 0 < s) (hq : q.IsAdmissible) :
(lambdaSq R s q a)⁻¹ ≤ multiscaleDescendantWeight Q k s * (lambdaSq Q s q a)⁻¹
source
theorem HCPolySupport.Book.Ch02.ThetaRatio_nonneg {d : ℕ} (Q : TriadicCube d) (a : TriadicCoeffFamily d) {s t : ℝ} (hs : 0 < s) (ht : 0 < t) :
0 ≤ ThetaRatio Q s t a
source
theorem HCPolySupport.Book.Ch02.one_le_ThetaRatio_of_pos {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {s t : ℝ} (hs : 0 < s) (ht : 0 < t) :
1 ≤ ThetaRatio Q s t a
source
theorem HCPolySupport.Book.Ch02.one_le_ThetaRatio {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {s t : ℝ} (ht : 0 < t) (hts : t < s) :
1 ≤ ThetaRatio Q s t a
source
theorem HCPolySupport.Book.Ch02.descendant_ThetaRatio_le {d : ℕ} [NeZero d] {Q R : TriadicCube d} {k : ℤ} (a : TriadicCoeffFamily d) {s t : ℝ} (hR : R ∈ descendantsAtScale Q k) (hs : 0 < s) (ht : 0 < t) :
ThetaRatio R s t a ≤ multiscaleDescendantWeight Q k s * multiscaleDescendantWeight Q k t * ThetaRatio Q s t a
source
theorem HCPolySupport.Book.Ch02.descendant_ThetaRatio_rpow_half_le {d : ℕ} [NeZero d] {Q R : TriadicCube d} {k : ℤ} (a : TriadicCoeffFamily d) {s t : ℝ} (hR : R ∈ descendantsAtScale Q k) (hs : 0 < s) (ht : 0 < t) :
(ThetaRatio R s t a).rpow (1 / 2) ≤ (multiscaleDescendantWeight Q k s * multiscaleDescendantWeight Q k t * ThetaRatio Q s t a).rpow (1 / 2)