Coarse-graining support: #
Support.Deterministic.MultiscaleQuantitiesBasic.EllipticityFiniteQ.ScaleBounds
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.multiscale_ellipticity_lambdaSq_two_inv_le_of_half_of_ellipticField
{d : ℕ}
[NeZero d]
{Q R : TriadicCube d}
{k : ℤ}
(a : CoeffField d)
{s lam Lam : ℝ}
(hs : 0 < s)
(hR : R ∈ descendantsAtScale Q k)
(hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a)
(hData : OpenCubeDescendantDeterministicCoarseData Q a)
(hsum_half :
Summable fun (n : ℕ) =>
geometricWeight (s / 2) 2 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow 1)
:
theorem
HCPolySupport.multiscale_ellipticity_lambdaSq_two_inv_le_rpow_s_of_half_of_ellipticField
{d : ℕ}
[NeZero d]
{Q R : TriadicCube d}
{k : ℤ}
(a : CoeffField d)
{s lam Lam : ℝ}
(hs : 0 < s)
(hR : R ∈ descendantsAtScale Q k)
(hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a)
(hData : OpenCubeDescendantDeterministicCoarseData Q a)
(hsum_half :
Summable fun (n : ℕ) =>
geometricWeight (s / 2) 2 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow 1)
:
theorem
HCPolySupport.multiscale_ellipticity_LambdaSq_two_le_rpow_s_of_half_of_ellipticField
{d : ℕ}
[NeZero d]
{Q R : TriadicCube d}
{k : ℤ}
(a : CoeffField d)
{s lam Lam : ℝ}
(hs : 0 < s)
(hR : R ∈ descendantsAtScale Q k)
(hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a)
(hData : OpenCubeDescendantDeterministicCoarseData Q a)
(hsum_half :
Summable fun (n : ℕ) => geometricWeight (s / 2) 2 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow 1)
:
Half-scale upper-ellipticity localization for the finite-q = 2
multiscale coefficient.
theorem
HCPolySupport.multiscale_ellipticity_LambdaSq_finite_descendantsAtScale_le
{d : ℕ}
(Q : TriadicCube d)
{k : ℤ}
(hk : k ≤ Q.scale)
(a : CoeffField d)
(s q : ℝ)
(hs : 0 ≤ s)
(hq : 0 < q)
(hsum :
Summable fun (n : ℕ) => geometricWeight s q n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (q / 2))
:
(finsetSsup (descendantsAtScale Q k) fun (R : TriadicCube d) => LambdaSq R s (MultiscaleExponent.finite q) a) ≤ Real.rpow 3 (2 * s * ↑(Q.scale - k).toNat) * LambdaSq Q s (MultiscaleExponent.finite q) a
theorem
HCPolySupport.multiscale_ellipticity_lambdaSq_finite_inv_descendantsAtScale_le
{d : ℕ}
(Q : TriadicCube d)
{k : ℤ}
(hk : k ≤ Q.scale)
(a : CoeffField d)
(s q : ℝ)
(hs : 0 ≤ s)
(hq : 0 < q)
(hsum :
Summable fun (n : ℕ) =>
geometricWeight s q n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (q / 2))
:
(finsetSsup (descendantsAtScale Q k) fun (R : TriadicCube d) => (lambdaSq R s (MultiscaleExponent.finite q) a)⁻¹) ≤ Real.rpow 3 (2 * s * ↑(Q.scale - k).toNat) * (lambdaSq Q s (MultiscaleExponent.finite q) a)⁻¹
theorem
HCPolySupport.multiscale_ellipticity_finite_scale_bounds
{d : ℕ}
(Q : TriadicCube d)
{k : ℤ}
(hk : k ≤ Q.scale)
(a : CoeffField d)
(s q : ℝ)
(hs : 0 ≤ s)
(hq : 0 < q)
(hBsum :
Summable fun (n : ℕ) => geometricWeight s q n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (q / 2))
(hSigmaSum :
Summable fun (n : ℕ) =>
geometricWeight s q n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (q / 2))
:
(finsetSsup (descendantsAtScale Q k) fun (R : TriadicCube d) => LambdaSq R s (MultiscaleExponent.finite q) a) ≤ Real.rpow 3 (2 * s * ↑(Q.scale - k).toNat) * LambdaSq Q s (MultiscaleExponent.finite q) a ∧ (finsetSsup (descendantsAtScale Q k) fun (R : TriadicCube d) => (lambdaSq R s (MultiscaleExponent.finite q) a)⁻¹) ≤ Real.rpow 3 (2 * s * ↑(Q.scale - k).toNat) * (lambdaSq Q s (MultiscaleExponent.finite q) a)⁻¹
theorem
HCPolySupport.multiscale_ellipticity_finite_basic_properties_of_isEllipticFieldOn_of_isSigmaCoarse
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
{t s q lam Lam : ℝ}
(hq : 0 < q)
(ht : 0 < t)
(hts : t < s)
(hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a)
(hData : OpenCubeDescendantDeterministicCoarseData Q a)
(hBsum_t :
Summable fun (n : ℕ) => geometricWeight t q n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (q / 2))
(hSigmaSum_t :
Summable fun (n : ℕ) =>
geometricWeight t q n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (q / 2))
:
(lambdaSq Q s (MultiscaleExponent.finite q) a)⁻¹ ≤ (lambdaSq Q t (MultiscaleExponent.finite q) a)⁻¹ ∧ coarseSigmaStarInvBlockNorm Q a ≤ (lambdaSq Q s (MultiscaleExponent.finite q) a)⁻¹ ∧ coarseBBlockNorm Q a ≤ LambdaSq Q s (MultiscaleExponent.finite q) a ∧ LambdaSq Q s (MultiscaleExponent.finite q) a ≤ LambdaSq Q t (MultiscaleExponent.finite q) a ∧ ∀ {k : ℤ},
k ≤ Q.scale →
(finsetSsup (descendantsAtScale Q k) fun (R : TriadicCube d) =>
LambdaSq R s (MultiscaleExponent.finite q) a) ≤ Real.rpow 3 (2 * s * ↑(Q.scale - k).toNat) * LambdaSq Q s (MultiscaleExponent.finite q) a ∧ (finsetSsup (descendantsAtScale Q k) fun (R : TriadicCube d) =>
(lambdaSq R s (MultiscaleExponent.finite q) a)⁻¹) ≤ Real.rpow 3 (2 * s * ↑(Q.scale - k).toNat) * (lambdaSq Q s (MultiscaleExponent.finite q) a)⁻¹