Coarse-graining support: Support.Book.Ch05.Theorems.Section52.GeometrySeries.SmallTailTerm #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.Book.Ch05.Section52.upperSmallTailTerm_le_raw_unitDescendantSup
{d : ℕ}
[NeZero d]
(m : ℕ)
{s r : ℝ}
(hs : 0 < s)
(hsr : s < r)
(hr : r < 1)
(a : RegCoeffField d)
:
let D := descendantsAtScale (originCube d ↑m) 0;
have hD := ⋯;
upperSmallSqrtTailCoeffField m r a ^ 2 / section52SmallTailWeight r m ≤ (25 * s⁻¹ * (r - s)⁻¹ * Real.rpow 3 (-r * ↑m)) ^ 2 / section52SmallTailWeight r m * D.sup' hD fun (U : TriadicCube d) => Ch04.LambdaSqCoeffField U s (Ch02.MultiscaleExponent.finite 1) a
theorem
HCPolySupport.Book.Ch05.Section52.lowerSmallTailTerm_le_raw_unitDescendantSup
{d : ℕ}
[NeZero d]
(m : ℕ)
{s r : ℝ}
(hs : 0 < s)
(hsr : s < r)
(hr : r < 1)
(a : RegCoeffField d)
:
let D := descendantsAtScale (originCube d ↑m) 0;
have hD := ⋯;
lowerSmallSqrtTailCoeffField m r a ^ 2 / section52SmallTailWeight r m ≤ (25 * s⁻¹ * (r - s)⁻¹ * Real.rpow 3 (-r * ↑m)) ^ 2 / section52SmallTailWeight r m * D.sup' hD fun (U : TriadicCube d) => (Ch04.lambdaSqCoeffField U s (Ch02.MultiscaleExponent.finite 1) a)⁻¹
theorem
HCPolySupport.Book.Ch05.Section52.upperSmallTailTerm_le_sameExponent_unitDescendantSum
{d : ℕ}
[NeZero d]
(m : ℕ)
{s : ℝ}
(hs : 0 < s)
(a : RegCoeffField d)
:
have D := descendantsAtScale (originCube d ↑m) 0;
have V := section52SmallTailWeight s m;
upperSmallSqrtTailCoeffField m s a ^ 2 / V ≤ Real.rpow 3 (-s * ↑m) ^ 2 * ↑D.card / V * ∑ U ∈ D, Ch04.LambdaSqCoeffField U s (Ch02.MultiscaleExponent.finite 1) a
theorem
HCPolySupport.Book.Ch05.Section52.lowerSmallTailTerm_le_sameExponent_unitDescendantSum
{d : ℕ}
[NeZero d]
(m : ℕ)
{s : ℝ}
(hs : 0 < s)
(a : RegCoeffField d)
:
have D := descendantsAtScale (originCube d ↑m) 0;
have V := section52SmallTailWeight s m;
lowerSmallSqrtTailCoeffField m s a ^ 2 / V ≤ Real.rpow 3 (-s * ↑m) ^ 2 * ↑D.card / V * ∑ U ∈ D, (Ch04.lambdaSqCoeffField U s (Ch02.MultiscaleExponent.finite 1) a)⁻¹