Coarse-graining support: Support.Book.Ch02.Theorems.MultiscaleEllipticity.Finite.Properties #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Finite-exponent multiscale ellipticity: public properties #
theorem
HCPolySupport.Book.Ch02.LambdaSq_finite_nonneg
{d : ℕ}
(Q : TriadicCube d)
(a : TriadicCoeffFamily d)
{s q : ℝ}
(hs : 0 < s)
(hq : 1 ≤ q)
:
theorem
HCPolySupport.Book.Ch02.lambdaSq_finite_nonneg
{d : ℕ}
(Q : TriadicCube d)
(a : TriadicCoeffFamily d)
{s q : ℝ}
(hs : 0 < s)
(hq : 1 ≤ q)
:
theorem
HCPolySupport.Book.Ch02.summable_geometricWeight_one_mul_maxDescendantBMatrixNormAtScale
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : TriadicCoeffFamily d)
{s : ℝ}
(hs : 0 < s)
:
Summable fun (n : ℕ) => geometricWeight s 1 n * maxDescendantBMatrixNormAtScale Q (Q.scale - ↑n) a
The q=1 upper operator-norm series is summable for every Ch2 triadic coefficient family.
theorem
HCPolySupport.Book.Ch02.summable_geometricWeight_one_mul_maxDescendantSigmaStarInvMatrixNormAtScale
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : TriadicCoeffFamily d)
{s : ℝ}
(hs : 0 < s)
:
Summable fun (n : ℕ) => geometricWeight s 1 n * maxDescendantSigmaStarInvMatrixNormAtScale Q (Q.scale - ↑n) a
The q=1 lower inverse operator-norm series is summable for every Ch2 triadic coefficient family.
theorem
HCPolySupport.Book.Ch02.LambdaSq_finite_one_le_tsum_weighted_maxDescendantBMatrixNormAtScale
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : TriadicCoeffFamily d)
{s : ℝ}
(hs : 0 < s)
:
LambdaSq Q s (MultiscaleExponent.finite 1) a ≤ ∑' (n : ℕ), geometricWeight s 1 n * maxDescendantBMatrixNormAtScale Q (Q.scale - ↑n) a
Jensen upper bound for the q=1 Ch2 upper operator multiscale ellipticity.
The norm here is Ch02.matrixNorm through
maxDescendantBMatrixNormAtScale.
theorem
HCPolySupport.Book.Ch02.lambdaSq_finite_one_inv_le_tsum_weighted_maxDescendantSigmaStarInvMatrixNormAtScale
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : TriadicCoeffFamily d)
{s : ℝ}
(hs : 0 < s)
:
(lambdaSq Q s (MultiscaleExponent.finite 1) a)⁻¹ ≤ ∑' (n : ℕ), geometricWeight s 1 n * maxDescendantSigmaStarInvMatrixNormAtScale Q (Q.scale - ↑n) a
Jensen upper bound for the q=1 Ch2 lower inverse operator multiscale
ellipticity. The norm here is Ch02.matrixNorm through
maxDescendantSigmaStarInvMatrixNormAtScale.
theorem
HCPolySupport.Book.Ch02.LambdaSqFinite_le_change_exponent
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : TriadicCoeffFamily d)
{s p q : ℝ}
(hs : 0 < s)
(hs_le : s ≤ 1)
(hp : 1 ≤ p)
(hpq : p ≤ q)
:
theorem
HCPolySupport.Book.Ch02.lambdaSqFinite_inv_le_change_exponent
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : TriadicCoeffFamily d)
{s p q : ℝ}
(hs : 0 < s)
(hs_le : s ≤ 1)
(hp : 1 ≤ p)
(hpq : p ≤ q)
:
theorem
HCPolySupport.Book.Ch02.oneCube_b_le_LambdaSq_finite
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : TriadicCoeffFamily d)
{s q : ℝ}
(hs : 0 < s)
(hq : 1 ≤ q)
:
theorem
HCPolySupport.Book.Ch02.oneCube_sigmaStarInv_le_lambdaSq_finite_inv
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : TriadicCoeffFamily d)
{s q : ℝ}
(hs : 0 < s)
(hq : 1 ≤ q)
:
theorem
HCPolySupport.Book.Ch02.coarseBMatrixNorm_pos
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : TriadicCoeffFamily d)
:
theorem
HCPolySupport.Book.Ch02.coarseSigmaStarInvMatrixNorm_pos
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : TriadicCoeffFamily d)
:
theorem
HCPolySupport.Book.Ch02.LambdaSq_finite_pos
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : TriadicCoeffFamily d)
{s q : ℝ}
(hs : 0 < s)
(hq : 1 ≤ q)
:
theorem
HCPolySupport.Book.Ch02.lambdaSq_finite_pos
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : TriadicCoeffFamily d)
{s q : ℝ}
(hs : 0 < s)
(hq : 1 ≤ q)
:
theorem
HCPolySupport.Book.Ch02.oneCube_sigmaStarInv_le_b
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : TriadicCoeffFamily d)
:
theorem
HCPolySupport.Book.Ch02.LambdaSq_finite_antitone
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : TriadicCoeffFamily d)
{t s q : ℝ}
(ht : 0 < t)
(hts : t < s)
(hq : 1 ≤ q)
:
theorem
HCPolySupport.Book.Ch02.lambdaSq_finite_mono
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : TriadicCoeffFamily d)
{t s q : ℝ}
(ht : 0 < t)
(hts : t < s)
(hq : 1 ≤ q)
:
theorem
HCPolySupport.Book.Ch02.lambdaSq_finite_le_oneCube
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : TriadicCoeffFamily d)
{s q : ℝ}
(hs : 0 < s)
(hq : 1 ≤ q)
: