Coarse-graining support: Support.Deterministic.MultiscaleQuantitiesBasic.Ellipticity.ScaleBounds #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.coarseBBlockNorm_le_inv_geometricWeight_sq_mul_LambdaSq_one_of_mem_descendantsAtScale
{d : ℕ}
{Q R : TriadicCube d}
{k : ℤ}
(a : CoeffField d)
(s : ℝ)
(hs : 0 < s)
(hR : R ∈ descendantsAtScale Q k)
(hsum :
Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
:
coarseBBlockNorm R a ≤ (geometricWeight s 1 (Q.scale - k).toNat ^ 2)⁻¹ * LambdaSq Q s (MultiscaleExponent.finite 1) a
theorem
HCPolySupport.coarseSigmaStarInvBlockNorm_le_weighted_lambdaInv
{d : ℕ}
{Q R : TriadicCube d}
{k : ℤ}
(a : CoeffField d)
(s : ℝ)
(hs : 0 < s)
(hR : R ∈ descendantsAtScale Q k)
(hsum :
Summable fun (n : ℕ) =>
geometricWeight s 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
:
coarseSigmaStarInvBlockNorm R a ≤ (geometricWeight s 1 (Q.scale - k).toNat ^ 2)⁻¹ * (lambdaSq Q s (MultiscaleExponent.finite 1) a)⁻¹
theorem
HCPolySupport.maxDescendantBBlockNormAtScale_le_inv_geometricWeight_sq_mul_LambdaSq_one
{d : ℕ}
(Q : TriadicCube d)
{k : ℤ}
(hk : k ≤ Q.scale)
(a : CoeffField d)
(s : ℝ)
(hs : 0 < s)
(hsum :
Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
:
maxDescendantBBlockNormAtScale Q k a ≤ (geometricWeight s 1 (Q.scale - k).toNat ^ 2)⁻¹ * LambdaSq Q s (MultiscaleExponent.finite 1) a
theorem
HCPolySupport.maxDescendantSigmaStarInvNormAtScale_le_inv_geometricWeight_sq_mul_lambdaSq_one_inv
{d : ℕ}
(Q : TriadicCube d)
{k : ℤ}
(hk : k ≤ Q.scale)
(a : CoeffField d)
(s : ℝ)
(hs : 0 < s)
(hsum :
Summable fun (n : ℕ) =>
geometricWeight s 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
:
maxDescendantSigmaStarInvNormAtScale Q k a ≤ (geometricWeight s 1 (Q.scale - k).toNat ^ 2)⁻¹ * (lambdaSq Q s (MultiscaleExponent.finite 1) a)⁻¹
theorem
HCPolySupport.multiscale_ellipticity_q1_normalized_scale_bounds
{d : ℕ}
(Q : TriadicCube d)
{k : ℤ}
(hk : k ≤ Q.scale)
(a : CoeffField d)
(s : ℝ)
(hs : 0 < s)
(hBsum :
Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
(hSigmaSum :
Summable fun (n : ℕ) =>
geometricWeight s 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
:
maxDescendantBBlockNormAtScale Q k a ≤ (geometricWeight s 1 (Q.scale - k).toNat ^ 2)⁻¹ * LambdaSq Q s (MultiscaleExponent.finite 1) a ∧ (finsetSsup (descendantsAtScale Q k) fun (R : TriadicCube d) => LambdaSq R s (MultiscaleExponent.finite 1) a) ≤ Real.rpow 3 (2 * s * ↑(Q.scale - k).toNat) * LambdaSq Q s (MultiscaleExponent.finite 1) a ∧ maxDescendantSigmaStarInvNormAtScale Q k a ≤ (geometricWeight s 1 (Q.scale - k).toNat ^ 2)⁻¹ * (lambdaSq Q s (MultiscaleExponent.finite 1) a)⁻¹ ∧ (finsetSsup (descendantsAtScale Q k) fun (R : TriadicCube d) =>
(lambdaSq R s (MultiscaleExponent.finite 1) a)⁻¹) ≤ Real.rpow 3 (2 * s * ↑(Q.scale - k).toNat) * (lambdaSq Q s (MultiscaleExponent.finite 1) a)⁻¹
theorem
HCPolySupport.multiscale_ellipticity_q1_normalized_basic_properties_of_isEllipticFieldOn_of_isSigmaCoarse
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
{t s lam Lam : ℝ}
(ht : 0 < t)
(hts : t < s)
(hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a)
(hData : OpenCubeDescendantDeterministicCoarseData Q a)
(hBsum_t :
Summable fun (n : ℕ) => geometricWeight t 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
(hSigmaSum_t :
Summable fun (n : ℕ) =>
geometricWeight t 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
:
coarseSigmaStarInvBlockNorm Q a ≤ (lambdaSq Q s (MultiscaleExponent.finite 1) a)⁻¹ ∧ (lambdaSq Q s (MultiscaleExponent.finite 1) a)⁻¹ ≤ (lambdaSq Q t (MultiscaleExponent.finite 1) a)⁻¹ ∧ coarseBBlockNorm Q a ≤ LambdaSq Q s (MultiscaleExponent.finite 1) a ∧ LambdaSq Q s (MultiscaleExponent.finite 1) a ≤ LambdaSq Q t (MultiscaleExponent.finite 1) a ∧ ∀ {k : ℤ},
k ≤ Q.scale →
maxDescendantBBlockNormAtScale Q k a ≤ (geometricWeight s 1 (Q.scale - k).toNat ^ 2)⁻¹ * LambdaSq Q s (MultiscaleExponent.finite 1) a ∧ (finsetSsup (descendantsAtScale Q k) fun (R : TriadicCube d) =>
LambdaSq R s (MultiscaleExponent.finite 1) a) ≤ Real.rpow 3 (2 * s * ↑(Q.scale - k).toNat) * LambdaSq Q s (MultiscaleExponent.finite 1) a ∧ maxDescendantSigmaStarInvNormAtScale Q k a ≤ (geometricWeight s 1 (Q.scale - k).toNat ^ 2)⁻¹ * (lambdaSq Q s (MultiscaleExponent.finite 1) a)⁻¹ ∧ (finsetSsup (descendantsAtScale Q k) fun (R : TriadicCube d) =>
(lambdaSq R s (MultiscaleExponent.finite 1) a)⁻¹) ≤ Real.rpow 3 (2 * s * ↑(Q.scale - k).toNat) * (lambdaSq Q s (MultiscaleExponent.finite 1) a)⁻¹