Rectangular partial summation on a finite indexed carrier

The coordinate map need not be injective: repeated coordinates, arithmetic coefficients, and all support masks stay inside the original carrier sums.

noncomputable def LiLiuPrereqFouvry.Rectangle.coordinatePrefix {α : Type u_1} {ι : Type u_2} [Fintype ι] (s : Finset α) (coord : α → ι → ℕ) (a : α → ℂ) (cap : ι → ℕ) : ℂ

A genuine coordinate rectangle cut out of the original finite carrier.

Equations

• LiLiuPrereqFouvry.Rectangle.coordinatePrefix s coord a cap = ∑ t ∈ s with ∀ (i : ι), coord t i ≤ cap i, a t

noncomputable def LiLiuPrereqFouvry.Rectangle.coordinatePrefixMax {α : Type u_1} {ι : Type u_2} [Fintype ι] (lo hi : ι → ℕ) (s : Finset α) (coord : α → ι → ℕ) (a : α → ℂ) : ℝ

The explicitly constructed maximum over all upper corners of the enclosing box.

Equations

• LiLiuPrereqFouvry.Rectangle.coordinatePrefixMax lo hi s coord a = ↑((LiLiuPrereqFouvry.Rectangle.box lo hi).sup fun (cap : ι → ℕ) => ‖LiLiuPrereqFouvry.Rectangle.coordinatePrefix s coord a cap‖₊)

theorem LiLiuPrereqFouvry.Rectangle.coordinatePrefix_norm_le_max {α : Type u_1} {ι : Type u_2} [Fintype ι] (lo hi : ι → ℕ) (s : Finset α) (coord : α → ι → ℕ) (a : α → ℂ) (cap : ι → ℕ) (hcap : cap ∈ box lo hi) : ‖coordinatePrefix s coord a cap‖ ≤ coordinatePrefixMax lo hi s coord a

theorem LiLiuPrereqFouvry.Rectangle.coordinatePrefixMax_nonneg {α : Type u_1} {ι : Type u_2} [Fintype ι] (lo hi : ι → ℕ) (s : Finset α) (coord : α → ι → ℕ) (a : α → ℂ) : 0 ≤ coordinatePrefixMax lo hi s coord a

theorem LiLiuPrereqFouvry.Rectangle.summation_by_parts_coordinates {α : Type u_1} {ι : Type u_2} [Fintype ι] (lo hi : ι → ℕ) (s : Finset α) (coord : α → ι → ℕ) (w : (ι → ℕ) → ℂ) (a : α → ℂ) (hcoord : ∀ t ∈ s, coord t ∈ box lo hi) : ∑ t ∈ s, w (coord t) * a t = ∑ cap ∈ box lo hi, mixedDifference lo hi w cap * coordinatePrefix s coord a cap

Finite multivariate summation by parts on the original indexed carrier. Only the smooth weight is differenced; no injectivity or coefficient bound is used.

theorem LiLiuPrereqFouvry.Rectangle.norm_coordinate_sum_le_of_prefix_bound {α : Type u_1} {ι : Type u_2} [Fintype ι] (lo hi : ι → ℕ) (s : Finset α) (coord : α → ι → ℕ) (w : (ι → ℕ) → ℂ) (a : α → ℂ) (hcoord : ∀ t ∈ s, coord t ∈ box lo hi) (B : ℝ) (hB : ∀ cap ∈ box lo hi, ‖coordinatePrefix s coord a cap‖ ≤ B) : ‖∑ t ∈ s, w (coord t) * a t‖ ≤ variation lo hi w * B

A uniform bound for the arithmetic rectangular prefixes can be applied directly, without first reasoning about the finite maximum.

theorem LiLiuPrereqFouvry.Rectangle.norm_coordinate_sum_le_variation_mul_max {α : Type u_1} {ι : Type u_2} [Fintype ι] (lo hi : ι → ℕ) (s : Finset α) (coord : α → ι → ℕ) (w : (ι → ℕ) → ℂ) (a : α → ℂ) (hcoord : ∀ t ∈ s, coord t ∈ box lo hi) : ‖∑ t ∈ s, w (coord t) * a t‖ ≤ variation lo hi w * coordinatePrefixMax lo hi s coord a

Rectangle-prefix maximum inequality, retaining the original indexed carrier.

theorem LiLiuPrereqFouvry.Rectangle.norm_coordinate_sum_five_le {α : Type u_1} (lo hi : Fin 5 → ℕ) (s : Finset α) (coord : α → Fin 5 → ℕ) (w : (Fin 5 → ℕ) → ℂ) (a : α → ℂ) (hcoord : ∀ t ∈ s, ∀ (i : Fin 5), lo i ≤ coord t i ∧ coord t i ≤ hi i) : ‖∑ t ∈ s, w (coord t) * a t‖ ≤ variation lo hi w * coordinatePrefixMax lo hi s coord a

Five-coordinate finite-carrier version used by the extracted dispersion phase.