Finite-order algebra for the parametrix remainder

This module proves the numerical reindexing behind paper (3.20)--(3.21). It is independent of the analytic content of Proposition 3.4: once an order-by-order identity is supplied, the low counterterms cancel with multiplicity one and precisely the pairs m + 2q > A remain.

theorem Anderson4D.lowCountertermSum_eq_flat {R : Type u_1} [AddCommMonoid R] (A : ℕ) (C : ℕ → ℕ → R) : ∑ m ∈ Finset.Icc 1 A, ∑ q ∈ Finset.Icc 1 A with 2 * q ≤ m, C q (m - 2 * q) = ∑ p ∈ (Finset.Icc 1 A).product (Finset.Icc 1 A) with 2 * p.2 ≤ p.1, C p.2 (p.1 - 2 * p.2)

Flatten the low-counterterm order/rank sum to a product finset.

theorem Anderson4D.lowCountertermPairs_eq_flat {R : Type u_1} [AddCommMonoid R] (A : ℕ) (C : ℕ → ℕ → R) : ∑ r ∈ Finset.range (A + 1), ∑ q ∈ Finset.Icc 1 A with r + 2 * q ≤ A, C q r = ∑ p ∈ (Finset.range (A + 1)).product (Finset.Icc 1 A) with p.1 + 2 * p.2 ≤ A, C p.2 p.1

Flatten the equivalent low region in remainder coordinates.

theorem Anderson4D.lowCountertermFlat_reindex {R : Type u_1} [AddCommMonoid R] (A : ℕ) (C : ℕ → ℕ → R) : ∑ p ∈ (Finset.Icc 1 A).product (Finset.Icc 1 A) with 2 * p.2 ≤ p.1, C p.2 (p.1 - 2 * p.2) = ∑ p ∈ (Finset.range (A + 1)).product (Finset.Icc 1 A) with p.1 + 2 * p.2 ≤ A, C p.2 p.1

The change of variables r = m - 2q is a multiplicity-one bijection between the two descriptions of the low counterterm region.

theorem Anderson4D.lowCountertermOrder_reindex {R : Type u_1} [AddCommMonoid R] (A : ℕ) (C : ℕ → ℕ → R) : ∑ m ∈ Finset.Icc 1 A, ∑ q ∈ Finset.Icc 1 A with 2 * q ≤ m, C q (m - 2 * q) = ∑ r ∈ Finset.range (A + 1), ∑ q ∈ Finset.Icc 1 A with r + 2 * q ≤ A, C q r

Reindex the low counterterms from the order appearing in Proposition 3.4 to the (tail order, counterterm order) coordinates used by (3.20).

theorem Anderson4D.totalCounterterm_eq_low_add_boundary {R : Type u_1} [AddCommMonoid R] (A : ℕ) (C : ℕ → ℕ → R) : ∑ r ∈ Finset.range (A + 1), ∑ q ∈ Finset.Icc 1 A, C q r = ∑ r ∈ Finset.range (A + 1), ∑ q ∈ Finset.Icc 1 A with r + 2 * q ≤ A, C q r + ∑ r ∈ Finset.range (A + 1), ∑ q ∈ Finset.Icc 1 A with ¬r + 2 * q ≤ A, C q r

Split all counterterms into the cancelling low region and the boundary region r + 2q > A of paper (3.21).

theorem Anderson4D.sum_range_succ_eq_sum_Icc {R : Type u_1} [AddCommMonoid R] (A : ℕ) (f : ℕ → R) : ∑ k ∈ Finset.range A, f (k + 1) = ∑ m ∈ Finset.Icc 1 A, f m

Reindex the positive orders 1,...,A by k ↦ k+1.

theorem Anderson4D.countertermFilter_eq_Icc_half {m A : ℕ} (hm : m ≤ A) : {q ∈ Finset.Icc 1 A | 2 * q ≤ m} = Finset.Icc 1 (m / 2)

For an order m ≤ A, the globally bounded filter used by the telescope is exactly the paper range 1 ≤ q ≤ m/2.

theorem Anderson4D.parametrixTelescope {R : Type u_1} [AddCommGroup R] (A : ℕ) (P N : ℕ → R) (C : ℕ → ℕ → R) (hN : ∀ m ∈ Finset.Icc 1 A, N (m - 1) = P m + ∑ q ∈ Finset.Icc 1 A with 2 * q ≤ m, C q (m - 2 * q)) : ∑ m ∈ Finset.range (A + 1), P m - ∑ m ∈ Finset.range (A + 1), N m + ∑ r ∈ Finset.range (A + 1), ∑ q ∈ Finset.Icc 1 A, C q r = P 0 - N A + ∑ r ∈ Finset.range (A + 1), ∑ q ∈ Finset.Icc 1 A with ¬r + 2 * q ≤ A, C q r

Abstract telescoping form of paper (3.20)--(3.21).

Here P m is the order-m parametrix contribution, N m is the noise composition at order m, and C q r is the order-2q counterterm acting on P r.

theorem Anderson4D.parametrixTelescopeIcc {R : Type u_1} [AddCommGroup R] (A : ℕ) (P N : ℕ → R) (C : ℕ → ℕ → R) (hN : ∀ m ∈ Finset.Icc 1 A, N (m - 1) = P m + ∑ q ∈ Finset.Icc 1 (m / 2), C q (m - 2 * q)) : ∑ m ∈ Finset.range (A + 1), P m - ∑ m ∈ Finset.range (A + 1), N m + ∑ r ∈ Finset.range (A + 1), ∑ q ∈ Finset.Icc 1 A, C q r = P 0 - N A + ∑ r ∈ Finset.range (A + 1), ∑ q ∈ Finset.Icc 1 A with ¬r + 2 * q ≤ A, C q r

Paper-indexed form of parametrixTelescope, with the counterterm range written exactly as 1 ≤ q ≤ m/2.