Coarse-graining support: Support.Book.Ch05.Theorems.Section52.Coefficients.RootCoeff #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.Book.Ch05.Section52.section52LargeScaleLpRootCoeff_eq_const_mul_decay_mul_gap_rpow
{d ξ : ℕ}
{s : ℝ}
{m : ℕ}
{n : ℤ}
(hn : n ∈ section52LargeScaleSet m)
:
theorem
HCPolySupport.Book.Ch05.Section52.section52LargeScaleSqrtRootCoeff_eq_const_mul_decay_mul_gap_rpow
{d ξ : ℕ}
{s : ℝ}
{m : ℕ}
{n : ℤ}
(hn : n ∈ section52LargeScaleSet m)
:
theorem
HCPolySupport.Book.Ch05.Section52.section52LargeScaleLpRootCoeff_scale_sum_le_geometricDiscount
{d ξ : ℕ}
{s : ℝ}
(m : ℕ)
(hs : 0 ≤ s)
(hgap : 0 < ↑d - s)
:
∑ n ∈ section52LargeScaleSet m, section52LargeScaleLpRootCoeff d ξ s m n ≤ 2 * Ch04.rosenthalDescendantsAtScaleLpConst d 0 ξ * geometricDiscount s 1 * Real.rpow 3 (-(s - ↑d / ↑ξ) * ↑m) * (geometricDiscount (↑d - s) 1)⁻¹
theorem
HCPolySupport.Book.Ch05.Section52.section52LargeScaleSqrtRootCoeff_scale_sum_le_geometricDiscount
{d ξ : ℕ}
{s : ℝ}
(m : ℕ)
(hs : 0 ≤ s)
(hgap : 0 < ↑d / 2 + ↑d / ↑ξ - s)
:
∑ n ∈ section52LargeScaleSet m, section52LargeScaleSqrtRootCoeff d ξ s m n ≤ 2 * Ch04.rosenthalDescendantsAtScaleSqrtConst d 0 ξ * geometricDiscount s 1 * Real.rpow 3 (-(s - ↑d / ↑ξ) * ↑m) * (geometricDiscount (↑d / 2 + ↑d / ↑ξ - s) 1)⁻¹
theorem
HCPolySupport.Book.Ch05.Section52.section52LargeScaleRootCoeff_scale_sum_le_geometricDiscount
{d ξ : ℕ}
{s : ℝ}
(m : ℕ)
(hs : 0 ≤ s)
(hgapLp : 0 < ↑d - s)
(hgapSqrt : 0 < ↑d / 2 + ↑d / ↑ξ - s)
:
∑ n ∈ section52LargeScaleSet m, section52LargeScaleRootCoeff d ξ s m n ≤ (2 * Ch04.rosenthalDescendantsAtScaleLpConst d 0 ξ * geometricDiscount s 1 * (geometricDiscount (↑d - s) 1)⁻¹ + 2 * Ch04.rosenthalDescendantsAtScaleSqrtConst d 0 ξ * geometricDiscount s 1 * (geometricDiscount (↑d / 2 + ↑d / ↑ξ - s) 1)⁻¹) * Real.rpow 3 (-(s - ↑d / ↑ξ) * ↑m)
theorem
HCPolySupport.Book.Ch05.Section52.section52LargeScaleRootCoeff_scale_sum_le_momentBoundCoeff
{d ξ : ℕ}
[NeZero d]
{s : ℝ}
(m : ℕ)
(hξ_one : 1 ≤ ↑ξ)
(hξ_two : 2 ≤ ↑ξ)
(hs : 0 ≤ s)
(hs_lt_one : s < 1)
(hgapSqrt : 0 < ↑d / 2 + ↑d / ↑ξ - s)
:
↑(Fintype.card (Fin d)) * ↑(Fintype.card (Fin d)) * ∑ n ∈ section52LargeScaleSet m, section52LargeScaleRootCoeff d ξ s m n ≤ section52MomentBoundCoeff d ξ (section52LargeScalarAbsorptionConst d) s m
theorem
HCPolySupport.Book.Ch05.Section52.section52SmallRawCoeff_eq
{d ξ m : ℕ}
{s r : ℝ}
(hr : 0 < r)
:
theorem
HCPolySupport.Book.Ch05.Section52.section52RawTwoExponentCoeff_le_twoExponentMomentBoundCoeff
{d ξ m : ℕ}
[NeZero d]
{s r : ℝ}
(hξ_one : 1 ≤ ξ)
(hξ_two : 2 ≤ ξ)
(hs : 0 < s)
(hsr : s < r)
(hr_lt_one : r < 1)
(hlargeGap : 0 < ↑d / 2 + ↑d / ↑ξ - r)
:
(25 * s⁻¹ * (r - s)⁻¹ * Real.rpow 3 (-r * ↑m)) ^ 2 / section52SmallTailWeight r m * ↑(descendantsAtScale (originCube d ↑m) 0).card ^ (1 / ↑ξ) + ↑(Fintype.card (Fin d)) * ↑(Fintype.card (Fin d)) * ∑ n ∈ section52LargeScaleSet m, section52LargeScaleRootCoeff d ξ r m n ≤ section52TwoExponentMomentBoundCoeff d ξ (625 + section52LargeScalarAbsorptionConst d) s r m