Coarse-graining support: Support.Book.Ch05.Theorems.Section52.GeometrySeries.TwoExponentBounds #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.Book.Ch05.Section52.upperSmallSqrtTailCoeffField_term_le_two_exponent
{d : ℕ}
[NeZero d]
(m j : ℕ)
{s r : ℝ}
(hs : 0 < s)
(hsr : s < r)
(a : RegCoeffField d)
:
geometricWeight r 1 (j + m) * (Ch04.maxDescendantBMatrixNormCoeffFieldAtScale (originCube d ↑m) (-↑j) a).rpow (1 / 2) ≤ (geometricDiscount s 1)⁻¹ * Real.rpow 3 (-(r - s) * ↑j) * Real.rpow 3 (-r * ↑m) * ((descendantsAtScale (originCube d ↑m) 0).sup' ⋯ fun (U : TriadicCube d) =>
Ch04.LambdaSqCoeffField U s (Ch02.MultiscaleExponent.finite 1) a).rpow
(1 / 2)
theorem
HCPolySupport.Book.Ch05.Section52.lowerSmallSqrtTailCoeffField_term_le_two_exponent
{d : ℕ}
[NeZero d]
(m j : ℕ)
{s r : ℝ}
(hs : 0 < s)
(hsr : s < r)
(a : RegCoeffField d)
:
geometricWeight r 1 (j + m) * (Ch04.maxDescendantSigmaStarInvMatrixNormCoeffFieldAtScale (originCube d ↑m) (-↑j) a).rpow (1 / 2) ≤ (geometricDiscount s 1)⁻¹ * Real.rpow 3 (-(r - s) * ↑j) * Real.rpow 3 (-r * ↑m) * ((descendantsAtScale (originCube d ↑m) 0).sup' ⋯ fun (U : TriadicCube d) =>
(Ch04.lambdaSqCoeffField U s (Ch02.MultiscaleExponent.finite 1) a)⁻¹).rpow
(1 / 2)
theorem
HCPolySupport.Book.Ch05.Section52.upperSmallSqrtTailCoeffField_le_two_exponent_unitCube_source
{d : ℕ}
[NeZero d]
(m : ℕ)
{s r : ℝ}
(hs : 0 < s)
(hsr : s < r)
(hr : r < 1)
(a : RegCoeffField d)
:
upperSmallSqrtTailCoeffField m r a ≤ 25 * s⁻¹ * (r - s)⁻¹ * Real.rpow 3 (-r * ↑m) * ((descendantsAtScale (originCube d ↑m) 0).sup' ⋯ fun (U : TriadicCube d) =>
Ch04.LambdaSqCoeffField U s (Ch02.MultiscaleExponent.finite 1) a).rpow
(1 / 2)
theorem
HCPolySupport.Book.Ch05.Section52.lowerSmallSqrtTailCoeffField_le_two_exponent_unitCube_source
{d : ℕ}
[NeZero d]
(m : ℕ)
{s r : ℝ}
(hs : 0 < s)
(hsr : s < r)
(hr : r < 1)
(a : RegCoeffField d)
:
lowerSmallSqrtTailCoeffField m r a ≤ 25 * s⁻¹ * (r - s)⁻¹ * Real.rpow 3 (-r * ↑m) * ((descendantsAtScale (originCube d ↑m) 0).sup' ⋯ fun (U : TriadicCube d) =>
(Ch04.lambdaSqCoeffField U s (Ch02.MultiscaleExponent.finite 1) a)⁻¹).rpow
(1 / 2)