Coarse-graining support: Support.Book.Ch04.PartitionAverageConstants

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

Coefficient-free constants for Chapter 4 partition averages

This module owns the numerical scales and color-count constants shared by the partition-average and descendant-average concentration APIs.

noncomputable def HCPolySupport.Book.Ch04.partitionCardinalityScale {d : ℕ} (n m : ℤ) : ℝ

Cardinal square-root fluctuation scale of a triadic partition.

Equations

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

noncomputable def HCPolySupport.Book.Ch04.gammaSigmaDescendantsAtScaleConst (d : ℕ) (k : ℤ) (σ : ℝ) : ℝ

Explicit color-count constant for descendant averages with Gamma_sigma tails.

Equations

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

noncomputable def HCPolySupport.Book.Ch04.psiSigmaDescendantsAtScaleConst (d : ℕ) (k : ℤ) (σ : ℝ) : ℝ

Explicit color-count constant for descendant averages with Psi_sigma tails.

Equations

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

noncomputable def HCPolySupport.Book.Ch04.rosenthalDescendantsAtScaleRpowLpConst (d : ℕ) (k : ℤ) (p : ℝ) : ℝ

Explicit color-count constant multiplying the real-exponent L^p Rosenthal term in a descendant-average bound.

Equations

• HCPolySupport.Book.Ch04.rosenthalDescendantsAtScaleRpowLpConst d k p = 2 * p * ↑(HCPolySupport.scaleColorPeriod k ^ d) ^ (1 - 1 / p)

noncomputable def HCPolySupport.Book.Ch04.rosenthalDescendantsAtScaleRpowSqrtConst (d : ℕ) (k : ℤ) (p : ℝ) : ℝ

Explicit color-count constant multiplying the square-function term in a real-exponent Rosenthal descendant-average bound.

Equations

• HCPolySupport.Book.Ch04.rosenthalDescendantsAtScaleRpowSqrtConst d k p = 4 * HCPolySupport.Book.Ch04.rosenthalBennettIntegralConst * (√p * √↑(HCPolySupport.scaleColorPeriod k ^ d))