Coarse-graining support: Support.Deterministic.MultiscaleQuantitiesBasic.EllipticityFiniteQ.Series #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Finite-q ellipticity and localization #
This file upgrades the Chapter-2 ellipticity surface from the first q = 1
lane to the finite-q statements actually present in the notes.
theorem
HCPolySupport.multiscale_ellipticity_LambdaSq_finite_formula
{d : ℕ}
(Q : TriadicCube d)
(s q : ℝ)
(a : CoeffField d)
:
LambdaSq Q s (MultiscaleExponent.finite q) a = (∑' (n : ℕ), geometricWeight s q n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (q / 2)).rpow (2 / q)
theorem
HCPolySupport.multiscale_ellipticity_lambdaSq_finite_formula
{d : ℕ}
(Q : TriadicCube d)
(s q : ℝ)
(a : CoeffField d)
:
lambdaSq Q s (MultiscaleExponent.finite q) a = (∑' (n : ℕ), geometricWeight s q n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (q / 2)).rpow
(-2 / q)
theorem
HCPolySupport.multiscale_ellipticity_LambdaSq_finite_series_nonneg
{d : ℕ}
(Q : TriadicCube d)
(s q : ℝ)
(a : CoeffField d)
(_hq : 0 ≤ q)
(hsq : 0 ≤ s * q)
:
theorem
HCPolySupport.multiscale_ellipticity_lambdaSq_finite_series_nonneg
{d : ℕ}
(Q : TriadicCube d)
(s q : ℝ)
(a : CoeffField d)
(_hq : 0 ≤ q)
(hsq : 0 ≤ s * q)
:
theorem
HCPolySupport.multiscale_ellipticity_LambdaSq_finite_nonneg
{d : ℕ}
(Q : TriadicCube d)
(s q : ℝ)
(a : CoeffField d)
(hq : 0 ≤ q)
(hsq : 0 ≤ s * q)
:
theorem
HCPolySupport.multiscale_ellipticity_lambdaSq_finite_nonneg
{d : ℕ}
(Q : TriadicCube d)
(s q : ℝ)
(a : CoeffField d)
(hq : 0 ≤ q)
(hsq : 0 ≤ s * q)
:
theorem
HCPolySupport.multiscale_ellipticity_LambdaSq_finite_rpow_q_div_two_eq_tsum
{d : ℕ}
(Q : TriadicCube d)
(s q : ℝ)
(a : CoeffField d)
(hq : 0 < q)
(hsq : 0 ≤ s * q)
:
(LambdaSq Q s (MultiscaleExponent.finite q) a).rpow (q / 2) = ∑' (n : ℕ), geometricWeight s q n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (q / 2)
theorem
HCPolySupport.multiscale_ellipticity_lambdaSq_finite_rpow_neg_q_div_two_eq_tsum
{d : ℕ}
(Q : TriadicCube d)
(s q : ℝ)
(a : CoeffField d)
(hq : 0 < q)
(hsq : 0 ≤ s * q)
:
theorem
HCPolySupport.coarseBBlockNorm_rpow_q_div_two_le_LambdaSq_finite_rpow_q_div_two
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
{s q lam Lam : ℝ}
(hs : 0 < s)
(hq : 0 < q)
(hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a)
(hData : OpenCubeDescendantDeterministicCoarseData Q a)
(hsum :
Summable fun (n : ℕ) => geometricWeight s q n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (q / 2))
:
theorem
HCPolySupport.coarseSigmaStarInvBlockNorm_rpow_q_div_two_le_lambdaSq_finite_rpow_neg_q_div_two
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
{s q lam Lam : ℝ}
(hs : 0 < s)
(hq : 0 < q)
(hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a)
(hData : OpenCubeDescendantDeterministicCoarseData Q a)
(hsum :
Summable fun (n : ℕ) =>
geometricWeight s q n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (q / 2))
:
(coarseSigmaStarInvBlockNorm Q a).rpow (q / 2) ≤ (lambdaSq Q s (MultiscaleExponent.finite q) a).rpow (-q / 2)
theorem
HCPolySupport.coarseBBlockNorm_le_LambdaSq_finite_of_isEllipticFieldOn_of_isSigmaCoarse
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
{s q lam Lam : ℝ}
(hs : 0 < s)
(hq : 0 < q)
(hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a)
(hData : OpenCubeDescendantDeterministicCoarseData Q a)
(hsum :
Summable fun (n : ℕ) => geometricWeight s q n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (q / 2))
:
theorem
HCPolySupport.coarseSigmaStarInvBlockNorm_le_lambdaSq_finite_inv_of_isEllipticFieldOn_of_isSigmaCoarse
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
{s q lam Lam : ℝ}
(hs : 0 < s)
(hq : 0 < q)
(hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a)
(hData : OpenCubeDescendantDeterministicCoarseData Q a)
(hsum :
Summable fun (n : ℕ) =>
geometricWeight s q n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (q / 2))
:
theorem
HCPolySupport.multiscale_LambdaSq_le_of_sigmaCoarse_elliptic
{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)
(hsum_t :
Summable fun (n : ℕ) => geometricWeight t q n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (q / 2))
:
(LambdaSq Q s (MultiscaleExponent.finite q) a).rpow (q / 2) ≤ (LambdaSq Q t (MultiscaleExponent.finite q) a).rpow (q / 2)
theorem
HCPolySupport.multiscale_ellipticity_LambdaSq_finite_le_of_lt_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)
(hsum_t :
Summable fun (n : ℕ) => geometricWeight t q n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (q / 2))
:
theorem
HCPolySupport.multiscale_ellipticity_lambdaSq_finite_rpow_neg_q_div_two_le
{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)
(hsum_t :
Summable fun (n : ℕ) =>
geometricWeight t q n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (q / 2))
:
theorem
HCPolySupport.multiscale_lambdaSq_inv_le_of_sigmaCoarse_elliptic
{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)
(hsum_t :
Summable fun (n : ℕ) =>
geometricWeight t q n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (q / 2))
: