Exact grouping and dissipation allocation for selected coefficient orders.

theorem AVenhance.Infra.Section4.IteratesFilteredGrouping.filtered_map_sum {α : Type u_1} (P : List α) (q : α → Bool) (f : α → ℝ) : (List.map f (List.filter q P)).sum = (List.map (fun (p : α) => if q p = true then f p else 0) P).sum

theorem AVenhance.Infra.Section4.iterateSpatialSplits_filtered_sum_by_two_orders (w : List (Fin 2)) (q : ℕ → Bool) (f : ℕ → ℕ → ℝ) : (List.map (fun (p : List (Fin 2) × List (Fin 2)) => f p.1.length p.2.length) (List.filter (fun (p : List (Fin 2) × List (Fin 2)) => q p.1.length) (iterateSpatialSplits w))).sum = ∑ j ∈ Finset.range (w.length + 1), ↑(w.length.choose j) * if q j = true then f j (w.length - j) else 0

A cutoff on coefficient order preserves each binomial multiplicity.

theorem AVenhance.Infra.Section4.iterateYoungWeight_filtered_sum_le {κ : ℝ} (hκ : 0 < κ) (w : List (Fin 2)) (q : ℕ → Bool) : (List.map (fun (p : List (Fin 2) × List (Fin 2)) => iterateYoungWeight κ w.length p.1.length) (List.filter (fun (p : List (Fin 2) × List (Fin 2)) => q p.1.length) (iterateSpatialSplits w))).sum ≤ κ / 8

Any selection of coefficient orders retains the uniform dissipation allocation of the full expansion.

theorem AVenhance.Infra.Section4.iterate_filtered_remainder_group_bound {κ : ℝ} (hκ : 0 < κ) (w : List (Fin 2)) (q : ℕ → Bool) (D E : ℕ → ℝ) (G : List (Fin 2) → ℝ) (hG : ∀ p ∈ List.filter (fun (p : List (Fin 2) × List (Fin 2)) => q p.1.length) (iterateSpatialSplits w), G p.2 ≤ E p.2.length) : (List.map (fun (p : List (Fin 2) × List (Fin 2)) => D p.1.length ^ 2 / iterateYoungWeight κ w.length p.1.length * G p.2) (List.filter (fun (p : List (Fin 2) × List (Fin 2)) => q p.1.length) (iterateSpatialSplits w))).sum ≤ 16 / κ * ∑ j ∈ Finset.range (w.length + 1), if q j = true then ↑(w.length.choose j) ^ 2 * 2 ^ j * D j ^ 2 * E (w.length - j) else 0

The Young remainder for selected orders has the same exact squared binomial weights as the full remainder.