Coarse-graining support: #
Support.Deterministic.MultiscaleQuantitiesBasic.EllipticityFiniteQ.Descendants
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.multiscale_ellipticity_LambdaSq_finite_rpow_q_div_two_le_of_mem_descendantsAtScale
{d : ℕ}
{Q R : TriadicCube d}
{k : ℤ}
(a : CoeffField d)
(s q : ℝ)
(hs : 0 ≤ s)
(hq : 0 < q)
(hR : R ∈ descendantsAtScale Q k)
(hsum :
Summable fun (n : ℕ) => geometricWeight s q n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (q / 2))
:
theorem
HCPolySupport.multiscale_ellipticity_LambdaSq_finite_le_of_mem_descendantsAtScale
{d : ℕ}
{Q R : TriadicCube d}
{k : ℤ}
(a : CoeffField d)
(s q : ℝ)
(hs : 0 ≤ s)
(hq : 0 < q)
(hR : R ∈ descendantsAtScale Q k)
(hsum :
Summable fun (n : ℕ) => geometricWeight s q n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (q / 2))
:
theorem
HCPolySupport.summable_geometricWeight_maxDescendantBBlockNormAtScale_rpow_q_div_two_of_mem_descendantsAtScale
{d : ℕ}
{Q R : TriadicCube d}
{k : ℤ}
(a : CoeffField d)
(s q : ℝ)
(hs : 0 ≤ s)
(hq : 0 < q)
(hR : R ∈ descendantsAtScale Q k)
(hsum :
Summable fun (n : ℕ) => geometricWeight s q n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (q / 2))
:
Summable fun (n : ℕ) => geometricWeight s q n * (maxDescendantBBlockNormAtScale R (R.scale - ↑n) a).rpow (q / 2)
A summable upper-ellipticity finite-q series remains summable after
restricting the base cube to a descendant.
theorem
HCPolySupport.multiscale_ellipticity_lambdaSq_finite_rpow_neg_q_div_two_le_of_mem_descendantsAtScale
{d : ℕ}
{Q R : TriadicCube d}
{k : ℤ}
(a : CoeffField d)
(s q : ℝ)
(hs : 0 ≤ s)
(hq : 0 < q)
(hR : R ∈ descendantsAtScale Q k)
(hsum :
Summable fun (n : ℕ) =>
geometricWeight s q n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (q / 2))
:
theorem
HCPolySupport.summable_geometricWeight_maxDescendantSigmaStarInvNormAtScale_of_mem_descendantsAtScale
{d : ℕ}
{Q R : TriadicCube d}
{k : ℤ}
(a : CoeffField d)
(s q : ℝ)
(hs : 0 ≤ s)
(hq : 0 < q)
(hR : R ∈ descendantsAtScale Q k)
(hsum :
Summable fun (n : ℕ) =>
geometricWeight s q n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (q / 2))
:
Summable fun (n : ℕ) => geometricWeight s q n * (maxDescendantSigmaStarInvNormAtScale R (R.scale - ↑n) a).rpow (q / 2)
theorem
HCPolySupport.multiscale_ellipticity_lambdaSq_finite_inv_le_of_mem_descendantsAtScale
{d : ℕ}
{Q R : TriadicCube d}
{k : ℤ}
(a : CoeffField d)
(s q : ℝ)
(hs : 0 ≤ s)
(hq : 0 < q)
(hR : R ∈ descendantsAtScale Q k)
(hsum :
Summable fun (n : ℕ) =>
geometricWeight s q n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (q / 2))
:
theorem
HCPolySupport.multiscale_ellipticity_LambdaSq_finite_le_of_ellipticField_of_isSigmaCoarse
{d : ℕ}
[NeZero d]
{Q R : TriadicCube d}
{k : ℤ}
(a : CoeffField d)
{t s q lam Lam : ℝ}
(hq : 0 < q)
(ht : 0 < t)
(hts : t < s)
(hR : R ∈ descendantsAtScale Q k)
(hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a)
(hData : OpenCubeDescendantDeterministicCoarseData Q a)
(hsum_t :
Summable fun (n : ℕ) => geometricWeight t q n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (q / 2))
:
theorem
HCPolySupport.multiscale_ellipticity_lambdaSq_finite_inv_le_of_ellipticField
{d : ℕ}
[NeZero d]
{Q R : TriadicCube d}
{k : ℤ}
(a : CoeffField d)
{t s q lam Lam : ℝ}
(hq : 0 < q)
(ht : 0 < t)
(hts : t < s)
(hR : R ∈ descendantsAtScale Q k)
(hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a)
(hData : OpenCubeDescendantDeterministicCoarseData Q a)
(hsum_t :
Summable fun (n : ℕ) =>
geometricWeight t q n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (q / 2))
: