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

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

Infinite-Depth Chapter 2.5 Multiscale Ellipticity

This file proves the q = infinity boundedness, positivity, monotonicity, and one-cube comparison lemmas.

theorem HCPolySupport.Book.Ch02.LambdaSqInfinity_valueSet_bddAbove {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {s : ℝ} (hs : 0 ≤ s) : BddAbove {M : ℝ | ∃ (n : ℕ), M = Real.rpow 3 (-2 * s * ↑n) * maxDescendantBMatrixNormAtScale Q (Q.scale - ↑n) a}

theorem HCPolySupport.Book.Ch02.lambdaSqInfinity_denominator_valueSet_bddAbove {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {s : ℝ} (hs : 0 ≤ s) : BddAbove {M : ℝ | ∃ (n : ℕ), M = Real.rpow 3 (-2 * s * ↑n) * maxDescendantSigmaStarInvMatrixNormAtScale Q (Q.scale - ↑n) a}

theorem HCPolySupport.Book.Ch02.oneCube_b_le_LambdaSq_infinity {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {s : ℝ} (hs : 0 < s) : coarseBMatrixNorm Q a ≤ LambdaSq Q s MultiscaleExponent.infinity a

theorem HCPolySupport.Book.Ch02.LambdaSq_infinity_pos {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {s : ℝ} (hs : 0 < s) : 0 < LambdaSq Q s MultiscaleExponent.infinity a

theorem HCPolySupport.Book.Ch02.LambdaSq_infinity_nonneg {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {s : ℝ} (hs : 0 < s) : 0 ≤ LambdaSq Q s MultiscaleExponent.infinity a

theorem HCPolySupport.Book.Ch02.lambdaSqInfinity_denominator_pos {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {s : ℝ} (hs : 0 < s) : 0 < sSup {M : ℝ | ∃ (n : ℕ), M = Real.rpow 3 (-2 * s * ↑n) * maxDescendantSigmaStarInvMatrixNormAtScale Q (Q.scale - ↑n) a}

theorem HCPolySupport.Book.Ch02.lambdaSq_infinity_pos {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {s : ℝ} (hs : 0 < s) : 0 < lambdaSq Q s MultiscaleExponent.infinity a

theorem HCPolySupport.Book.Ch02.lambdaSq_infinity_nonneg {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {s : ℝ} (hs : 0 < s) : 0 ≤ lambdaSq Q s MultiscaleExponent.infinity a

theorem HCPolySupport.Book.Ch02.lambdaSq_infinity_le_oneCube {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {s : ℝ} (hs : 0 < s) : lambdaSq Q s MultiscaleExponent.infinity a ≤ (coarseSigmaStarInvMatrixNorm Q a)⁻¹

theorem HCPolySupport.Book.Ch02.LambdaSq_infinity_antitone {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {t s : ℝ} (ht : 0 < t) (hts : t < s) : LambdaSq Q s MultiscaleExponent.infinity a ≤ LambdaSq Q t MultiscaleExponent.infinity a

theorem HCPolySupport.Book.Ch02.lambdaSqInfinity_denominator_antitone {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {t s : ℝ} (ht : 0 < t) (hts : t < s) : sSup {M : ℝ | ∃ (n : ℕ), M = Real.rpow 3 (-2 * s * ↑n) * maxDescendantSigmaStarInvMatrixNormAtScale Q (Q.scale - ↑n) a} ≤ sSup {M : ℝ | ∃ (n : ℕ), M = Real.rpow 3 (-2 * t * ↑n) * maxDescendantSigmaStarInvMatrixNormAtScale Q (Q.scale - ↑n) a}

theorem HCPolySupport.Book.Ch02.lambdaSq_infinity_mono {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {t s : ℝ} (ht : 0 < t) (hts : t < s) : lambdaSq Q t MultiscaleExponent.infinity a ≤ lambdaSq Q s MultiscaleExponent.infinity a

theorem HCPolySupport.Book.Ch02.oneCube_sigmaStarInv_le_lambdaSq_infinity_inv {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : TriadicCoeffFamily d) {s : ℝ} (hs : 0 < s) : coarseSigmaStarInvMatrixNorm Q a ≤ (lambdaSq Q s MultiscaleExponent.infinity a)⁻¹