Coarse-graining support: Support.Book.Ch05.Theorems.Section52.Coefficients.Constants

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Section 5.2 internals: Coefficients

Coefficient absorption and large-scale root coefficients.

noncomputable def HCPolySupport.Book.Ch05.Section52.section52LargeScalarAbsorptionConst (d : ℕ) : ℝ

Dimension-only factor absorbing the large-scale scalar coefficients after extracting the moment exponent and reciprocal exponent gap.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.Book.Ch05.Section52.section52LargeScalarAbsorptionConst_nonneg (d : ℕ) : 0 ≤ section52LargeScalarAbsorptionConst d

theorem HCPolySupport.Book.Ch05.Section52.section52_rosenthalDescendantsAtScaleLpConst_zero_le_color_mul_xi {d ξ : ℕ} (hξ : 1 ≤ ↑ξ) : Ch04.rosenthalDescendantsAtScaleLpConst d 0 ξ ≤ 2 * ↑ξ * ↑(scaleColorPeriod 0 ^ d)

theorem HCPolySupport.Book.Ch05.Section52.section52_rosenthalDescendantsAtScaleSqrtConst_zero_le_color_mul_xi {d ξ : ℕ} (hξ : 1 ≤ ↑ξ) : Ch04.rosenthalDescendantsAtScaleSqrtConst d 0 ξ ≤ 4 * Ch04.rosenthalBennettIntegralConst * √↑(scaleColorPeriod 0 ^ d) * ↑ξ

theorem HCPolySupport.Book.Ch05.Section52.section52LargeScalarAbsorptionConst_absorbs {d ξ : ℕ} [NeZero d] {s : ℝ} (hξ_one : 1 ≤ ↑ξ) (hξ_two : 2 ≤ ↑ξ) (hs : 0 ≤ s) (hs_lt_one : s < 1) (hlargeGap : 0 < ↑d / 2 + ↑d / ↑ξ - s) : ↑(Fintype.card (Fin d)) * ↑(Fintype.card (Fin d)) * (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)⁻¹) ≤ section52LargeScalarAbsorptionConst d * (↑ξ * (↑d / 2 + ↑d / ↑ξ - s)⁻¹)

theorem HCPolySupport.Book.Ch05.Section52.section52MomentBoundCoeff_nonneg {d ξ m : ℕ} {C s : ℝ} (hC : 0 ≤ C) (hDenom : 0 < ↑d / 2 + ↑d / ↑ξ - s) : 0 ≤ section52MomentBoundCoeff d ξ C s m

The displayed Section 5.2 positive-excess coefficient is nonnegative.

theorem HCPolySupport.Book.Ch05.Section52.section52WidetildeThetaErrorCoeff_nonneg {d ξ m : ℕ} {C sMin : ℝ} (hC : 0 ≤ C) : 0 ≤ section52WidetildeThetaErrorCoeff d ξ C sMin m

The displayed Section 5.2 widetildeTheta error coefficient is nonnegative.

theorem HCPolySupport.Book.Ch05.Section52.section52MomentBoundCoeff_le_common_scale {d ξ m : ℕ} {C s sMin : ℝ} (hξ : 1 ≤ ξ) (hC : 0 ≤ C) (hDenom : 0 < ↑d / 2 + ↑d / ↑ξ - s) (hsMin_le : sMin ≤ s) : section52MomentBoundCoeff d ξ C s m ≤ C / (↑d / 2 + ↑d / ↑ξ - s) * ↑ξ ^ 2 * Real.rpow 3 (-(sMin - ↑d / ↑ξ) * ↑m)

A displayed Section 5.2 positive-excess coefficient is bounded by the common widetildeTheta scale whenever its exponent is at least the common minimum exponent.

theorem HCPolySupport.Book.Ch05.Section52.section52MomentBoundCoeff_mul_le_common_scale {d ξ m : ℕ} {CUpper CLower sUpper sLower : ℝ} (hCUpper : 0 ≤ CUpper) (hCLower : 0 ≤ CLower) (hsUpper_gt : ↑d / ↑ξ < sUpper) (hsLower_gt : ↑d / ↑ξ < sLower) (hUpperDenom : 0 < ↑d / 2 + ↑d / ↑ξ - sUpper) (hLowerDenom : 0 < ↑d / 2 + ↑d / ↑ξ - sLower) : section52MomentBoundCoeff d ξ CUpper sUpper m * section52MomentBoundCoeff d ξ CLower sLower m ≤ CUpper / (↑d / 2 + ↑d / ↑ξ - sUpper) * (CLower / (↑d / 2 + ↑d / ↑ξ - sLower)) * ↑ξ ^ 2 * Real.rpow 3 (-(min sUpper sLower - ↑d / ↑ξ) * ↑m)

The product of the two displayed Section 5.2 positive-excess coefficients is also bounded by the common widetildeTheta scale.

theorem HCPolySupport.Book.Ch05.Section52.section52_coefficients_mixed_le_widetildeThetaErrorCoeff {d ξ m : ℕ} {CUpper CLower CTheta sUpper sLower : ℝ} (hξ : 1 ≤ ξ) (hCUpper : 0 ≤ CUpper) (hCLower : 0 ≤ CLower) (hsUpper_gt : ↑d / ↑ξ < sUpper) (hsLower_gt : ↑d / ↑ξ < sLower) (hUpperDenom : 0 < ↑d / 2 + ↑d / ↑ξ - sUpper) (hLowerDenom : 0 < ↑d / 2 + ↑d / ↑ξ - sLower) (hCTheta : CUpper / (↑d / 2 + ↑d / ↑ξ - sUpper) + CLower / (↑d / 2 + ↑d / ↑ξ - sLower) + CUpper / (↑d / 2 + ↑d / ↑ξ - sUpper) * (CLower / (↑d / 2 + ↑d / ↑ξ - sLower)) ≤ CTheta) : section52MomentBoundCoeff d ξ CUpper sUpper m + section52MomentBoundCoeff d ξ CLower sLower m + section52MomentBoundCoeff d ξ CUpper sUpper m * section52MomentBoundCoeff d ξ CLower sLower m ≤ section52WidetildeThetaErrorCoeff d ξ CTheta (min sUpper sLower) m

Coefficient absorption for the final displayed Section 5.2 widetildeTheta estimate.

noncomputable def HCPolySupport.Book.Ch05.Section52.section52UnitDescendantRosenthalBudget {d : ℕ} (Q : TriadicCube d) (ξ : ℕ) (K : ℝ) : ℝ

The one-parent Rosenthal budget for unit-descendant averages over Q. This is a private coefficient used to feed the Ch4 law-facing finite-parent fluctuation theorem.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.Book.Ch05.Section52.section52UnitDescendantRosenthalBudget_nonneg {d : ℕ} (Q : TriadicCube d) (ξ : ℕ) {K : ℝ} (hK : 0 ≤ K) : 0 ≤ section52UnitDescendantRosenthalBudget Q ξ K

noncomputable def HCPolySupport.Book.Ch05.Section52.section52LargeScaleLpRootCoeff (d ξ : ℕ) (s : ℝ) (m : ℕ) (n : ℤ) : ℝ

The weighted large-scale root coefficient from the Rosenthal Lp term, including descendant-count normalization.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch05.Section52.section52LargeScaleSqrtRootCoeff (d ξ : ℕ) (s : ℝ) (m : ℕ) (n : ℤ) : ℝ

The weighted large-scale root coefficient from the Rosenthal square-root term, including descendant-count normalization.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch05.Section52.section52LargeScaleRootCoeff (d ξ : ℕ) (s : ℝ) (m : ℕ) (n : ℤ) : ℝ

The combined Lp and square-root contributions to the large-scale root coefficient.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.Book.Ch05.Section52.section52LargeScaleLpRootCoeff_nonneg {d ξ : ℕ} {s : ℝ} (m : ℕ) (n : ℤ) (hs : 0 ≤ s) : 0 ≤ section52LargeScaleLpRootCoeff d ξ s m n

theorem HCPolySupport.Book.Ch05.Section52.section52LargeScaleSqrtRootCoeff_nonneg {d ξ : ℕ} {s : ℝ} (m : ℕ) (n : ℤ) (hs : 0 ≤ s) : 0 ≤ section52LargeScaleSqrtRootCoeff d ξ s m n

theorem HCPolySupport.Book.Ch05.Section52.section52LargeScaleRootCoeff_nonneg {d ξ : ℕ} {s : ℝ} (m : ℕ) (n : ℤ) (hs : 0 ≤ s) : 0 ≤ section52LargeScaleRootCoeff d ξ s m n