Finite rectangular partial summation

The coefficients in this file are completely arbitrary. In particular, arithmetic coefficients, phases, and nonrectangular support indicators belong in a, not in the weight. The difference kernel is the tensor product of forward differences, with the weight extended by zero outside the box.

noncomputable def LiLiuPrereqFouvry.Rectangle.box {ι : Type u_1} [Fintype ι] (lo hi : ι → ℕ) : Finset (ι → ℕ)

Closed natural-number box, including empty and singleton intervals.

Equations

• LiLiuPrereqFouvry.Rectangle.box lo hi = Fintype.piFinset fun (i : ι) => Finset.Icc (lo i) (hi i)

@[simp]

theorem LiLiuPrereqFouvry.Rectangle.mem_box {ι : Type u_1} [Fintype ι] (lo hi x : ι → ℕ) : x ∈ box lo hi ↔ ∀ (i : ι), lo i ≤ x i ∧ x i ≤ hi i

def LiLiuPrereqFouvry.Rectangle.differenceKernel (t u : ℕ) : ℂ

One coordinate of the zero-extended forward difference.

Equations

• LiLiuPrereqFouvry.Rectangle.differenceKernel t u = (if t = u then 1 else 0) - if t + 1 = u then 1 else 0

noncomputable def LiLiuPrereqFouvry.Rectangle.mixedDifference {ι : Type u_1} [Fintype ι] (lo hi : ι → ℕ) (w : (ι → ℕ) → ℂ) (t : ι → ℕ) : ℂ

Full mixed forward difference, with all upper faces anchored at zero.

Equations

• LiLiuPrereqFouvry.Rectangle.mixedDifference lo hi w t = ∑ u ∈ LiLiuPrereqFouvry.Rectangle.box lo hi, w u * ∏ i : ι, LiLiuPrereqFouvry.Rectangle.differenceKernel (t i) (u i)

noncomputable def LiLiuPrereqFouvry.Rectangle.rectanglePrefix {ι : Type u_1} [Fintype ι] (lo hi : ι → ℕ) (a : (ι → ℕ) → ℂ) (t : ι → ℕ) : ℂ

Unweighted rectangular prefix; a may already contain any support mask.

Equations

• LiLiuPrereqFouvry.Rectangle.rectanglePrefix lo hi a t = ∑ x ∈ LiLiuPrereqFouvry.Rectangle.box lo hi with x ≤ t, a x

noncomputable def LiLiuPrereqFouvry.Rectangle.variation {ι : Type u_1} [Fintype ι] (lo hi : ι → ℕ) (w : (ι → ℕ) → ℂ) : ℝ

Total anchored mixed finite-difference variation.

Equations

• LiLiuPrereqFouvry.Rectangle.variation lo hi w = ∑ t ∈ LiLiuPrereqFouvry.Rectangle.box lo hi, ‖LiLiuPrereqFouvry.Rectangle.mixedDifference lo hi w t‖

noncomputable def LiLiuPrereqFouvry.Rectangle.prefixMax {ι : Type u_1} [Fintype ι] (lo hi : ι → ℕ) (a : (ι → ℕ) → ℂ) : ℝ

Explicit finite maximum of the norms of all rectangular prefixes.

Equations

• LiLiuPrereqFouvry.Rectangle.prefixMax lo hi a = ↑((LiLiuPrereqFouvry.Rectangle.box lo hi).sup fun (t : ι → ℕ) => ‖LiLiuPrereqFouvry.Rectangle.rectanglePrefix lo hi a t‖₊)

theorem LiLiuPrereqFouvry.Rectangle.rectanglePrefix_eq_box_min {ι : Type u_1} [Fintype ι] (lo hi : ι → ℕ) (a : (ι → ℕ) → ℂ) (t : ι → ℕ) : rectanglePrefix lo hi a t = ∑ x ∈ box lo fun (i : ι) => min (hi i) (t i), a x

These really are rectangular prefixes, with coordinatewise truncation.

theorem LiLiuPrereqFouvry.Rectangle.rectanglePrefix_eq_box {ι : Type u_1} [Fintype ι] (lo hi : ι → ℕ) (a : (ι → ℕ) → ℂ) (t : ι → ℕ) (ht : ∀ (i : ι), t i ≤ hi i) : rectanglePrefix lo hi a t = ∑ x ∈ box lo t, a x

@[simp]

theorem LiLiuPrereqFouvry.Rectangle.box_self {ι : Type u_1} [Fintype ι] (x : ι → ℕ) : box x x = {x}

theorem LiLiuPrereqFouvry.Rectangle.box_eq_empty_iff {ι : Type u_1} [Fintype ι] (lo hi : ι → ℕ) : box lo hi = ∅ ↔ ∃ (i : ι), hi i < lo i

theorem LiLiuPrereqFouvry.Rectangle.reconstruct {ι : Type u_1} [Fintype ι] (lo hi : ι → ℕ) (w : (ι → ℕ) → ℂ) (x : ι → ℕ) (hx : x ∈ box lo hi) : ∑ t ∈ box x hi, mixedDifference lo hi w t = w x

The mixed differences telescope on every upper subrectangle.

theorem LiLiuPrereqFouvry.Rectangle.summation_by_parts {ι : Type u_1} [Fintype ι] (lo hi : ι → ℕ) (w a : (ι → ℕ) → ℂ) : ∑ x ∈ box lo hi, w x * a x = ∑ t ∈ box lo hi, mixedDifference lo hi w t * rectanglePrefix lo hi a t

Exact multidimensional summation by parts. Only w is differenced.

theorem LiLiuPrereqFouvry.Rectangle.prefix_norm_le_prefixMax {ι : Type u_1} [Fintype ι] (lo hi : ι → ℕ) (a : (ι → ℕ) → ℂ) (t : ι → ℕ) (ht : t ∈ box lo hi) : ‖rectanglePrefix lo hi a t‖ ≤ prefixMax lo hi a

theorem LiLiuPrereqFouvry.Rectangle.variation_nonneg {ι : Type u_1} [Fintype ι] (lo hi : ι → ℕ) (w : (ι → ℕ) → ℂ) : 0 ≤ variation lo hi w

theorem LiLiuPrereqFouvry.Rectangle.prefixMax_nonneg {ι : Type u_1} [Fintype ι] (lo hi : ι → ℕ) (a : (ι → ℕ) → ℂ) : 0 ≤ prefixMax lo hi a

theorem LiLiuPrereqFouvry.Rectangle.norm_sum_le_variation_mul_prefixMax {ι : Type u_1} [Fintype ι] (lo hi : ι → ℕ) (w a : (ι → ℕ) → ℂ) : ‖∑ x ∈ box lo hi, w x * a x‖ ≤ variation lo hi w * prefixMax lo hi a

Rectangle-prefix inequality with a constructed maximum, not an assumed bound.

def LiLiuPrereqFouvry.Rectangle.corner {ι : Type u_1} (t : ι → ℕ) (e : ι → Bool) : ι → ℕ

The upper vertex selected by a Boolean choice in every coordinate.

Equations

• LiLiuPrereqFouvry.Rectangle.corner t e i = t i + if e i = true then 1 else 0

def LiLiuPrereqFouvry.Rectangle.cornerSign {ι : Type u_1} [Fintype ι] (e : ι → Bool) : ℂ

Alternating sign of a cube vertex.

Equations

• LiLiuPrereqFouvry.Rectangle.cornerSign e = ∏ i : ι, if e i = true then -1 else 1

noncomputable def LiLiuPrereqFouvry.Rectangle.extendWeight {ι : Type u_1} [Fintype ι] (lo hi : ι → ℕ) (w : (ι → ℕ) → ℂ) (x : ι → ℕ) : ℂ

Extension by zero only concerns the weight outside its enclosing box.

Equations

• LiLiuPrereqFouvry.Rectangle.extendWeight lo hi w x = if x ∈ LiLiuPrereqFouvry.Rectangle.box lo hi then w x else 0

theorem LiLiuPrereqFouvry.Rectangle.mixedDifference_eq_corners {ι : Type u_1} [Fintype ι] (lo hi : ι → ℕ) (w : (ι → ℕ) → ℂ) (t : ι → ℕ) : mixedDifference lo hi w t = ∑ e : ι → Bool, cornerSign e * extendWeight lo hi w (corner t e)

The kernel definition is exactly the usual alternating 2^d-corner stencil. At an upper face, the zero extension produces the lower-order face difference.

theorem LiLiuPrereqFouvry.Rectangle.norm_sum_masked_le {ι : Type u_1} [Fintype ι] (lo hi : ι → ℕ) (s : Finset (ι → ℕ)) (hs : s ⊆ box lo hi) (w a : (ι → ℕ) → ℂ) : ‖∑ x ∈ s, w x * a x‖ ≤ variation lo hi w * prefixMax lo hi fun (x : ι → ℕ) => if x ∈ s then a x else 0

The preceding bound applies to any finite, possibly nonrectangular support. The exact support indicator remains inside each unweighted prefix.

theorem LiLiuPrereqFouvry.Rectangle.norm_sum_five_le (lo hi : Fin 5 → ℕ) (w a : (Fin 5 → ℕ) → ℂ) : ‖∑ x ∈ box lo hi, w x * a x‖ ≤ variation lo hi w * prefixMax lo hi a

Five-coordinate specialization for the dispersion consumer.