Coarse-graining support: Support.Book.Ch05.Theorems.Section52.GeometrySeries.DescendantCardinality

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

Section 5.2 internals: GeometrySeries

Descendant geometry, geometric series, and small-tail estimates.

theorem HCPolySupport.Book.Ch05.Section52.section52_descendantsAtScale_originCube_large_card (d m : ℕ) {n : ℤ} (hn : n ≤ ↑m) : (descendantsAtScale (originCube d ↑m) n).card = (3 ^ d) ^ (↑m - n).toNat

Cardinality of scale-n descendants of cu_m.

theorem HCPolySupport.Book.Ch05.Section52.section52_descendantsAtScale_originCube_large_card_rpow (d ξ m : ℕ) {n : ℤ} (hn : n ≤ ↑m) : ↑(descendantsAtScale (originCube d ↑m) n).card ^ (1 / ↑ξ) = Real.rpow 3 (↑d / ↑ξ * ↑(↑m - n).toNat)

Real 1 / xi root of the number of scale-n descendants of cu_m.

theorem HCPolySupport.Book.Ch05.Section52.section52_descendantsAtScale_originCube_int_zero_card (d : ℕ) {n : ℤ} (hn : 0 ≤ n) : (descendantsAtScale (originCube d n) 0).card = (3 ^ d) ^ n.toNat

Cardinality of unit descendants of a nonnegative-scale origin cube.

theorem HCPolySupport.Book.Ch05.Section52.section52_descendantsAtScale_originCube_int_zero_card_rpow (d ξ : ℕ) {n : ℤ} (hn : 0 ≤ n) : ↑(descendantsAtScale (originCube d n) 0).card ^ (1 / ↑ξ) = Real.rpow 3 (↑d / ↑ξ * ↑n.toNat)

Real 1 / xi root of the number of unit descendants of a scale-n cube.

theorem HCPolySupport.Book.Ch05.Section52.section52_descendantsAtScale_originCube_int_zero_card_sqrt (d : ℕ) {n : ℤ} (hn : 0 ≤ n) : √↑(descendantsAtScale (originCube d n) 0).card = Real.rpow 3 (↑d / 2 * ↑n.toNat)

Square root of the number of unit descendants of a scale-n cube.

theorem HCPolySupport.Book.Ch05.Section52.section52_descendantsAtScale_originCube_int_zero_card_inv (d : ℕ) {n : ℤ} (hn : 0 ≤ n) : (↑(descendantsAtScale (originCube d n) 0).card)⁻¹ = Real.rpow 3 (-↑d * ↑n.toNat)

Inverse of the number of unit descendants of a nonnegative-scale origin cube.

theorem HCPolySupport.Book.Ch05.Section52.section52LargeScaleSet_toNat_sub_add_toNat {m : ℕ} {n : ℤ} (hn : n ∈ section52LargeScaleSet m) : (↑m - n).toNat + n.toNat = m

For manuscript large scales, the q = 1 depth from cu_m to scale n plus the absolute scale n is exactly m.

theorem HCPolySupport.Book.Ch05.Section52.section52LargeScaleSet_toNat_injOn (m : ℕ) : Set.InjOn Int.toNat ↑(section52LargeScaleSet m)

Int.toNat is injective on the nonnegative manuscript large scales.

theorem HCPolySupport.Book.Ch05.Section52.summable_rpow_three_neg_mul_nat {gap : ℝ} (hgap : 0 < gap) : Summable fun (n : ℕ) => Real.rpow 3 (-gap * ↑n)

The raw geometric powers underlying q = 1 normalized weights are summable.

theorem HCPolySupport.Book.Ch05.Section52.tsum_rpow_three_neg_mul_nat_eq_inv_geometricDiscount {gap : ℝ} (hgap : 0 < gap) : ∑' (n : ℕ), Real.rpow 3 (-gap * ↑n) = (geometricDiscount gap 1)⁻¹

Closed form of the raw q = 1 geometric-power series.

theorem HCPolySupport.Book.Ch05.Section52.section52SmallTailWeight_eq_rpow {s : ℝ} (hs : 0 < s) (m : ℕ) : section52SmallTailWeight s m = Real.rpow 3 (-s * ↑m)

theorem HCPolySupport.Book.Ch05.Section52.section52LargeScaleSet_raw_rpow_sum_le_inv_geometricDiscount {gap : ℝ} (m : ℕ) (hgap : 0 < gap) : ∑ n ∈ section52LargeScaleSet m, Real.rpow 3 (-gap * ↑n.toNat) ≤ (geometricDiscount gap 1)⁻¹

The finite manuscript large-scale set is dominated by the full raw geometric tail with the same positive gap.

theorem HCPolySupport.Book.Ch05.Section52.geometricDiscount_one_le_one (s : ℝ) : geometricDiscount s 1 ≤ 1

A one-step geometric discount is always at most one.

theorem HCPolySupport.Book.Ch05.Section52.geometricWeight_one_le_inv_discount_mul_gap_decay_mul_geometricWeight {s r : ℝ} (hs : 0 < s) (_hsr : s < r) (N : ℕ) : geometricWeight r 1 N ≤ (geometricDiscount s 1)⁻¹ * Real.rpow 3 (-(r - s) * ↑N) * geometricWeight s 1 N

theorem HCPolySupport.Book.Ch05.Section52.inv_geometricDiscount_one_le_five_inv_of_pos_lt_one {s : ℝ} (hs : 0 < s) (hs_lt_one : s < 1) : (geometricDiscount s 1)⁻¹ ≤ 5 * s⁻¹

theorem HCPolySupport.Book.Ch05.Section52.upper_unitCube_source_rpow_half_nonneg {d : ℕ} (m : ℕ) {s : ℝ} (hs : 0 < s) (a : RegCoeffField d) : 0 ≤ ((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.lower_unitCube_source_rpow_half_nonneg {d : ℕ} (m : ℕ) {s : ℝ} (hs : 0 < s) (a : RegCoeffField d) : 0 ≤ ((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.translateCube_originCube_zero_eq_of_scale_zero {d : ℕ} (Q : TriadicCube d) (hQ : Q.scale = 0) : translateCube (Ch04.scaleTranslationShift 0 Q) (originCube d 0) = Q

theorem HCPolySupport.Book.Ch05.Section52.upper_unitDescendantSup_momentRoot_le_card_mul_origin {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) {s : ℝ} {ξ m : ℕ} (hs : 0 < s) (hξ_one : 1 ≤ ξ) (hSourceInt : MeasureTheory.Integrable (fun (a : RegCoeffField d) => Ch04.LambdaSqCoeffField (originCube d 0) s (Ch02.MultiscaleExponent.finite 1) a ^ ξ) P) : let D := descendantsAtScale (originCube d ↑m) 0; have hD := ⋯; (Ch04.annealedMomentRoot P ξ fun (a : RegCoeffField d) => D.sup' hD fun (U : TriadicCube d) => Ch04.LambdaSqCoeffField U s (Ch02.MultiscaleExponent.finite 1) a) ≤ ↑D.card ^ (1 / ↑ξ) * Ch04.LambdaMomentAtScale P 0 s ξ

theorem HCPolySupport.Book.Ch05.Section52.lower_unitDescendantSup_momentRoot_le_card_mul_origin {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) {s : ℝ} {ξ m : ℕ} (hs : 0 < s) (hξ_one : 1 ≤ ξ) (hSourceInt : MeasureTheory.Integrable (fun (a : RegCoeffField d) => (Ch04.lambdaSqCoeffField (originCube d 0) s (Ch02.MultiscaleExponent.finite 1) a)⁻¹ ^ ξ) P) : let D := descendantsAtScale (originCube d ↑m) 0; have hD := ⋯; (Ch04.annealedMomentRoot P ξ fun (a : RegCoeffField d) => D.sup' hD fun (U : TriadicCube d) => (Ch04.lambdaSqCoeffField U s (Ch02.MultiscaleExponent.finite 1) a)⁻¹) ≤ ↑D.card ^ (1 / ↑ξ) * Ch04.lambdaInvMomentAtScale P 0 s ξ