Coarse-graining support: Support.Deterministic.MultiscaleQuantitiesBasic.Ellipticity.Descendants #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.thetaRatio_eq_sq_mul_rpow_half_rpow_neg_half
{d : ℕ}
(Q : TriadicCube d)
(s t : ℝ)
(a : CoeffField d)
(hs : 0 ≤ s)
(ht : 0 ≤ t)
:
ThetaRatio Q s t a = ((LambdaSq Q s (MultiscaleExponent.finite 1) a).rpow (1 / 2) * (lambdaSq Q t (MultiscaleExponent.finite 1) a).rpow (-1 / 2)) ^ 2
theorem
HCPolySupport.thetaRatio_eq_sq_series_product
{d : ℕ}
(Q : TriadicCube d)
(s t : ℝ)
(a : CoeffField d)
(hs : 0 ≤ s)
(ht : 0 ≤ t)
:
ThetaRatio Q s t a = ((∑' (n : ℕ), geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) * ∑' (n : ℕ), geometricWeight t 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) ^ 2
theorem
HCPolySupport.thetaRatio_nonneg
{d : ℕ}
(Q : TriadicCube d)
(s t : ℝ)
(a : CoeffField d)
(hs : 0 ≤ s)
(ht : 0 ≤ t)
:
theorem
HCPolySupport.thetaRatio_rpow_half_eq_mul_rpow_half_rpow_neg_half
{d : ℕ}
(Q : TriadicCube d)
(s t : ℝ)
(a : CoeffField d)
(hs : 0 ≤ s)
(ht : 0 ≤ t)
:
(ThetaRatio Q s t a).rpow (1 / 2) = (LambdaSq Q s (MultiscaleExponent.finite 1) a).rpow (1 / 2) * (lambdaSq Q t (MultiscaleExponent.finite 1) a).rpow (-1 / 2)
theorem
HCPolySupport.multiscale_ellipticity_LambdaSq_one_rpow_half_le_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))
:
theorem
HCPolySupport.mem_descendantsAtScale_sub_nat_of_mem_descendantsAtDepth
{d : ℕ}
{Q R : TriadicCube d}
{j : ℕ}
(hR : R ∈ descendantsAtDepth Q j)
:
Convert a depth-j descendant membership into the corresponding
absolute-scale descendant membership.
theorem
HCPolySupport.summable_geometricWeight_maxDescendantBBlockNormAtScale_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))
:
Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale R (R.scale - ↑n) a).rpow (1 / 2)
A summable upper-ellipticity q = 1 series remains summable after
restricting the base cube to a descendant.
theorem
HCPolySupport.summable_geometricWeight_maxDescendantBBlockNormAtScale_of_mem_descendantsAtDepth
{d : ℕ}
{Q R : TriadicCube d}
{j : ℕ}
(a : CoeffField d)
(s : ℝ)
(hs : 0 ≤ s)
(hR : R ∈ descendantsAtDepth Q j)
(hsum :
Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
:
Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale R (R.scale - ↑n) a).rpow (1 / 2)
Depth-j form of
summable_geometricWeight_maxDescendantBBlockNormAtScale_of_mem_descendantsAtScale.
theorem
HCPolySupport.summable_geometricWeight_maxDescendantSigmaStarInvNormAtScale_of_mem_descendantsAtDepth
{d : ℕ}
{Q R : TriadicCube d}
{j : ℕ}
(a : CoeffField d)
(s : ℝ)
(hs : 0 ≤ s)
(hR : R ∈ descendantsAtDepth Q j)
(hsum :
Summable fun (n : ℕ) =>
geometricWeight s 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
:
Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantSigmaStarInvNormAtScale R (R.scale - ↑n) a).rpow (1 / 2)
Depth-j form of
summable_geometricWeight_maxDescendantSigmaStarInvNormAtScale_of_mem_descendantsAtScale.
theorem
HCPolySupport.multiscale_ellipticity_LambdaSq_one_rpow_half_le_of_mem_descendantsAtDepth
{d : ℕ}
{Q R : TriadicCube d}
{j : ℕ}
(a : CoeffField d)
(s : ℝ)
(hs : 0 ≤ s)
(hR : R ∈ descendantsAtDepth Q j)
(hsum :
Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
:
(LambdaSq R s (MultiscaleExponent.finite 1) a).rpow (1 / 2) ≤ Real.rpow 3 (s * ↑j) * (LambdaSq Q s (MultiscaleExponent.finite 1) a).rpow (1 / 2)
Depth-j form of the finite-q = 1 upper ellipticity localization.
theorem
HCPolySupport.multiscale_ellipticity_LambdaSq_one_le_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))
:
theorem
HCPolySupport.multiscale_ellipticity_lambdaSq_one_rpow_neg_half_le_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 * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
:
theorem
HCPolySupport.multiscale_ellipticity_lambdaSq_one_rpow_neg_half_le_of_mem_descendantsAtDepth
{d : ℕ}
{Q R : TriadicCube d}
{j : ℕ}
(a : CoeffField d)
(s : ℝ)
(hs : 0 ≤ s)
(hR : R ∈ descendantsAtDepth Q j)
(hsum :
Summable fun (n : ℕ) =>
geometricWeight s 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
:
(lambdaSq R s (MultiscaleExponent.finite 1) a).rpow (-1 / 2) ≤ Real.rpow 3 (s * ↑j) * (lambdaSq Q s (MultiscaleExponent.finite 1) a).rpow (-1 / 2)
Depth-j form of the finite-q = 1 lower ellipticity localization.
theorem
HCPolySupport.multiscale_ellipticity_lambdaSq_one_inv_le_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 * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
:
theorem
HCPolySupport.multiscale_ellipticity_LambdaSq_one_descendantsAtScale_le
{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))
:
(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_lambdaSq_one_inv_descendantsAtScale_le
{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))
:
(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.thetaRatio_rpow_half_le_of_mem_descendantsAtScale
{d : ℕ}
{Q R : TriadicCube d}
{k : ℤ}
(a : CoeffField d)
(s t : ℝ)
(hs : 0 ≤ s)
(ht : 0 ≤ t)
(hR : R ∈ descendantsAtScale Q k)
(hBsum :
Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
(hSigmaSum :
Summable fun (n : ℕ) =>
geometricWeight t 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
:
theorem
HCPolySupport.thetaRatio_rpow_half_le_of_mem_descendantsAtDepth
{d : ℕ}
{Q R : TriadicCube d}
{j : ℕ}
(a : CoeffField d)
(s t : ℝ)
(hs : 0 ≤ s)
(ht : 0 ≤ t)
(hR : R ∈ descendantsAtDepth Q j)
(hBsum :
Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
(hSigmaSum :
Summable fun (n : ℕ) =>
geometricWeight t 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
:
Depth-j form of the ThetaRatio square-root localization.
theorem
HCPolySupport.thetaRatio_le_of_mem_descendantsAtScale
{d : ℕ}
{Q R : TriadicCube d}
{k : ℤ}
(a : CoeffField d)
(s t : ℝ)
(hs : 0 ≤ s)
(ht : 0 ≤ t)
(hR : R ∈ descendantsAtScale Q k)
(hBsum :
Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
(hSigmaSum :
Summable fun (n : ℕ) =>
geometricWeight t 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
:
theorem
HCPolySupport.thetaRatio_rpow_half_descendantsAtScale_le
{d : ℕ}
(Q : TriadicCube d)
{k : ℤ}
(hk : k ≤ Q.scale)
(a : CoeffField d)
(s t : ℝ)
(hs : 0 ≤ s)
(ht : 0 ≤ t)
(hBsum :
Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
(hSigmaSum :
Summable fun (n : ℕ) =>
geometricWeight t 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
:
(finsetSsup (descendantsAtScale Q k) fun (R : TriadicCube d) => (ThetaRatio R s t a).rpow (1 / 2)) ≤ Real.rpow 3 ((s + t) * ↑(Q.scale - k).toNat) * (ThetaRatio Q s t a).rpow (1 / 2)
theorem
HCPolySupport.thetaRatio_descendantsAtScale_le
{d : ℕ}
(Q : TriadicCube d)
{k : ℤ}
(hk : k ≤ Q.scale)
(a : CoeffField d)
(s t : ℝ)
(hs : 0 ≤ s)
(ht : 0 ≤ t)
(hBsum :
Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
(hSigmaSum :
Summable fun (n : ℕ) =>
geometricWeight t 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
:
(finsetSsup (descendantsAtScale Q k) fun (R : TriadicCube d) => ThetaRatio R s t a) ≤ Real.rpow 3 (2 * (s + t) * ↑(Q.scale - k).toNat) * ThetaRatio Q s t a