Coarse-graining support: Support.Book.Ch05.Theorems.Section52.Weights

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

Section 5.2 internals: Weights

Large-scale weights and finite/tail decompositions.

def HCPolySupport.Book.Ch05.Section52.section52LargeScaleSet (m : ℕ) : Finset ℤ

The large scales appearing after the Section 5.2 Jensen split.

For a cube cu_m, a q = 1 series index l < m corresponds to the absolute scale m - l, hence to one of the manuscript large scales 1, ..., m.

Equations

• HCPolySupport.Book.Ch05.Section52.section52LargeScaleSet m = Finset.image (fun (l : ℕ) => ↑m - ↑l) (Finset.range m)

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

The q = 1 geometric weight transported from series depth to absolute scale.

Equations

• HCPolySupport.Book.Ch05.Section52.section52LargeScaleWeight s m n = HCPolySupport.geometricWeight s 1 (↑m - n).toNat

theorem HCPolySupport.Book.Ch05.Section52.section52LargeScaleSet_mem_nonneg {m : ℕ} {n : ℤ} (hn : n ∈ section52LargeScaleSet m) : 0 ≤ n

theorem HCPolySupport.Book.Ch05.Section52.section52LargeScaleSet_mem_pos {m : ℕ} {n : ℤ} (hn : n ∈ section52LargeScaleSet m) : 1 ≤ n

theorem HCPolySupport.Book.Ch05.Section52.section52LargeScaleSet_mem_le_m {m : ℕ} {n : ℤ} (hn : n ∈ section52LargeScaleSet m) : n ≤ ↑m

theorem HCPolySupport.Book.Ch05.Section52.section52LargeScaleWeight_nonneg {s : ℝ} (m : ℕ) (hs : 0 ≤ s) (n : ℤ) : 0 ≤ section52LargeScaleWeight s m n

theorem HCPolySupport.Book.Ch05.Section52.section52LargeScaleSet_injOn (m : ℕ) : Set.InjOn (fun (l : ℕ) => ↑m - ↑l) ↑(Finset.range m)

theorem HCPolySupport.Book.Ch05.Section52.section52LargeScaleWeight_sum_eq_prefix_sum (s : ℝ) (m : ℕ) : ∑ n ∈ section52LargeScaleSet m, section52LargeScaleWeight s m n = ∑ l ∈ Finset.range m, geometricWeight s 1 l

theorem HCPolySupport.Book.Ch05.Section52.section52LargeScaleWeight_sum_le_one {s : ℝ} (hs : 0 < s) (m : ℕ) : ∑ n ∈ section52LargeScaleSet m, section52LargeScaleWeight s m n ≤ 1

theorem HCPolySupport.Book.Ch05.Section52.section52LargeScaleSet_weighted_sum_eq_prefix_sum (s : ℝ) (m : ℕ) (F : ℤ → ℝ) : ∑ n ∈ section52LargeScaleSet m, section52LargeScaleWeight s m n * F n = ∑ l ∈ Finset.range m, geometricWeight s 1 l * F (↑m - ↑l)

Reindex a finite q = 1 depth-prefix sum as a sum over large absolute scales.

theorem HCPolySupport.Book.Ch05.Section52.section52_tsum_weighted_scale_function_eq_largeScaleSet_sum_add_tail (s : ℝ) (m : ℕ) (F : ℤ → ℝ) (hsum : Summable fun (l : ℕ) => geometricWeight s 1 l * F (↑m - ↑l)) : ∑' (l : ℕ), geometricWeight s 1 l * F (↑m - ↑l) = ∑ n ∈ section52LargeScaleSet m, section52LargeScaleWeight s m n * F n + ∑' (l : ℕ), geometricWeight s 1 (l + m) * F (↑m - ↑(l + m))

Exact large/small split of a q = 1 depth-indexed weighted series.

The first term is the finite manuscript large-scale sum over absolute scales 1, ..., m; the second term is the small-scale tail beginning at series depth m.

noncomputable def HCPolySupport.Book.Ch05.Section52.section52SmallTailWeight (s : ℝ) (m : ℕ) : ℝ

Total geometric weight of the small-scale tail starting at depth m.

Equations

• HCPolySupport.Book.Ch05.Section52.section52SmallTailWeight s m = ∑' (j : ℕ), HCPolySupport.geometricWeight s 1 (j + m)

theorem HCPolySupport.Book.Ch05.Section52.section52SmallTailWeight_nonneg {s : ℝ} (hs : 0 ≤ s) (m : ℕ) : 0 ≤ section52SmallTailWeight s m

theorem HCPolySupport.Book.Ch05.Section52.section52LargeScaleWeight_sum_add_smallTailWeight_eq_one {s : ℝ} (hs : 0 < s) (m : ℕ) : ∑ n ∈ section52LargeScaleSet m, section52LargeScaleWeight s m n + section52SmallTailWeight s m = 1

theorem HCPolySupport.Book.Ch05.Section52.section52SmallTailWeight_pos {s : ℝ} (hs : 0 < s) (m : ℕ) : 0 < section52SmallTailWeight s m