Cardinality-free partial summation for the coupled five-variable weight

The corner stencil is identified with the genuine mixed increments of the concrete normalized weight. Interior grid widths telescope, and upper faces contribute one endpoint mass per inactive coordinate. The final factor is at most 2^5; no arithmetic coefficient or mask is differentiated.

def LiLiuPrereqFouvry.Rectangle.activeCoordinates (b : Fin 5 → Bool) : List (Fin 5)

Equations

• LiLiuPrereqFouvry.Rectangle.activeCoordinates b = List.filter b [0, 1, 2, 3, 4]

def LiLiuPrereqFouvry.Rectangle.endpointDifference (b : Bool) (l h : ℝ) (f : ℝ → ℂ) : ℂ

Equations

• LiLiuPrereqFouvry.Rectangle.endpointDifference b l h f = if b = true then f l - f h else f l

def LiLiuPrereqFouvry.Rectangle.endpointCube (b : Fin 5 → Bool) (l h : Fin 5 → ℝ) (f : (Fin 5 → ℝ) → ℂ) : ℂ

Equations

• LiLiuPrereqFouvry.Rectangle.endpointCube b l h f = LiLiuPrereqFouvry.Rectangle.endpointDifference (b 0) (l 0) (h 0) fun (x0 : ℝ) => LiLiuPrereqFouvry.Rectangle.endpointDifference (b 1) (l 1) (h 1) fun (x1 : ℝ) => LiLiuPrereqFouvry.Rectangle.endpointDifference (b 2) (l 2) (h 2) fun (x2 : ℝ) => LiLiuPrereqFouvry.Rectangle.endpointDifference (b 3) (l 3) (h 3) fun (x3 : ℝ) => LiLiuPrereqFouvry.Rectangle.endpointDifference (b 4) (l 4) (h 4) fun (x4 : ℝ) => f ![x0, x1, x2, x3, x4]

theorem LiLiuPrereqFouvry.Rectangle.endpointCube_eq_boxDiff (b : Fin 5 → Bool) (l h : Fin 5 → ℝ) (f : (Fin 5 → ℝ) → ℂ) : endpointCube b l h f = (-1) ^ (activeCoordinates b).length * SlowFactor.boxDiff (activeCoordinates b) l h f l

theorem LiLiuPrereqFouvry.Rectangle.activeCoordinates_nodup (b : Fin 5 → Bool) : (activeCoordinates b).Nodup

theorem LiLiuPrereqFouvry.Rectangle.norm_endpointCube_eq (b : Fin 5 → Bool) (l h : Fin 5 → ℝ) (f : (Fin 5 → ℝ) → ℂ) : ‖endpointCube b l h f‖ = ‖SlowFactor.boxDiff (activeCoordinates b) l h f l‖

def LiLiuPrereqFouvry.Rectangle.gridPoint (g : Fin 5 → ℕ → ℝ) (t : Fin 5 → ℕ) : Fin 5 → ℝ

Equations

• LiLiuPrereqFouvry.Rectangle.gridPoint g t i = g i (t i)

theorem LiLiuPrereqFouvry.Rectangle.mixedDifference_eq_endpointCube (lo hi t : Fin 5 → ℕ) (ht : t ∈ box lo hi) (g : Fin 5 → ℕ → ℝ) (f : (Fin 5 → ℝ) → ℂ) : mixedDifference lo hi (fun (u : Fin 5 → ℕ) => f (gridPoint g u)) t = endpointCube (fun (i : Fin 5) => decide (t i < hi i)) (gridPoint g t) (gridPoint g fun (i : Fin 5) => min (t i + 1) (hi i)) f

Exact identification of all boundary-anchored differences with the local mixed increment; upper boundary coordinates are inactive.

theorem LiLiuPrereqFouvry.Rectangle.sideProduct_activeCoordinates (b : Fin 5 → Bool) (l h : Fin 5 → ℝ) : SlowFactor.sideProduct (activeCoordinates b) l h = ∏ i : Fin 5, if b i = true then h i - l i else 1

def LiLiuPrereqFouvry.Rectangle.cellMass (hi : ℕ) (g : ℕ → ℝ) (t : ℕ) : ℝ

The endpoint has mass one; each interior cell has its actual grid width.

Equations

• LiLiuPrereqFouvry.Rectangle.cellMass hi g t = if t < hi then g (t + 1) - g t else 1

theorem LiLiuPrereqFouvry.Rectangle.sum_cellMass (lo hi : ℕ) (h : lo ≤ hi) (g : ℕ → ℝ) : ∑ t ∈ Finset.Icc lo hi, cellMass hi g t = 1 + g hi - g lo

theorem LiLiuPrereqFouvry.Rectangle.norm_mixedDifference_normalizedWeight_le (A B V : ℝ) (hV : |A| + |B| ≤ V) (lo hi t : Fin 5 → ℕ) (ht : t ∈ box lo hi) (g : Fin 5 → ℕ → ℝ) (hg : ∀ (i : Fin 5), Monotone (g i)) (hlo : ∀ (i : Fin 5), 1 ≤ g i (lo i)) (hhi : ∀ (i : Fin 5), g i (hi i) ≤ 2) : ‖mixedDifference lo hi (fun (u : Fin 5 → ℕ) => SlowFactor.normalizedWeight A B (gridPoint g u)) t‖ ≤ 64 * (6 + 2 * Real.pi) ^ 5 * (1 + V) ^ 5 * ∏ i : Fin 5, cellMass (hi i) (g i) (t i)

The concrete coupled smooth weight satisfies the local anchored-difference estimate, with no regularity imposed on arithmetic coefficients.

theorem LiLiuPrereqFouvry.Rectangle.variation_normalizedWeight_le (A B V : ℝ) (hV : |A| + |B| ≤ V) (lo hi : Fin 5 → ℕ) (hbox : ∀ (i : Fin 5), lo i ≤ hi i) (g : Fin 5 → ℕ → ℝ) (hg : ∀ (i : Fin 5), Monotone (g i)) (hlo : ∀ (i : Fin 5), 1 ≤ g i (lo i)) (hhi : ∀ (i : Fin 5), g i (hi i) ≤ 2) : (variation lo hi fun (u : Fin 5 → ℕ) => SlowFactor.normalizedWeight A B (gridPoint g u)) ≤ 2048 * (6 + 2 * Real.pi) ^ 5 * (1 + V) ^ 5

Summing the genuine mixed derivative bounds over every cell and every upper face costs at most 2^5, independently of the number of integer grid points.

theorem LiLiuPrereqFouvry.Rectangle.variation_normalizedWeight_div_le (A B V : ℝ) (hV : |A| + |B| ≤ V) (lo hi : Fin 5 → ℕ) (hbox : ∀ (i : Fin 5), lo i ≤ hi i) (R : Fin 5 → ℝ) (hR : ∀ (i : Fin 5), 0 < R i) (hlo : ∀ (i : Fin 5), R i ≤ ↑(lo i)) (hhi : ∀ (i : Fin 5), ↑(hi i) ≤ 2 * R i) : (variation lo hi fun (u : Fin 5 → ℕ) => SlowFactor.normalizedWeight A B fun (i : Fin 5) => ↑(u i) / R i) ≤ 2048 * (6 + 2 * Real.pi) ^ 5 * (1 + V) ^ 5

Positive-reference normalization, convenient for actual dyadic rectangles.

theorem LiLiuPrereqFouvry.Rectangle.variation_singleton (x : Fin 5 → ℕ) (w : (Fin 5 → ℕ) → ℂ) : variation x x w = ‖w x‖

theorem LiLiuPrereqFouvry.Rectangle.variation_eq_zero_of_box_empty (lo hi : Fin 5 → ℕ) (w : (Fin 5 → ℕ) → ℂ) (h : box lo hi = ∅) : variation lo hi w = 0

theorem LiLiuPrereqFouvry.Rectangle.variation_normalizedWeight_div_le_all (A B V : ℝ) (hV : |A| + |B| ≤ V) (lo hi : Fin 5 → ℕ) (R : Fin 5 → ℝ) (hR : ∀ (i : Fin 5), 0 < R i) (hlo : ∀ (i : Fin 5), R i ≤ ↑(lo i)) (hhi : ∀ (i : Fin 5), ↑(hi i) ≤ 2 * R i) : (variation lo hi fun (u : Fin 5 → ℕ) => SlowFactor.normalizedWeight A B fun (i : Fin 5) => ↑(u i) / R i) ≤ 2048 * (6 + 2 * Real.pi) ^ 5 * (1 + V) ^ 5

The concrete arithmetic-grid estimate also covers empty boxes, without an endpoint-order premise. Singleton sides contribute their endpoint mass only.

theorem LiLiuPrereqFouvry.Rectangle.norm_coordinate_sum_normalizedWeight_le {α : Type u_1} (A B V : ℝ) (hV : |A| + |B| ≤ V) (lo hi : Fin 5 → ℕ) (hbox : ∀ (i : Fin 5), lo i ≤ hi i) (g : Fin 5 → ℕ → ℝ) (hg : ∀ (i : Fin 5), Monotone (g i)) (hlo : ∀ (i : Fin 5), 1 ≤ g i (lo i)) (hhi : ∀ (i : Fin 5), g i (hi i) ≤ 2) (s : Finset α) (coord : α → Fin 5 → ℕ) (a : α → ℂ) (hcoord : ∀ t ∈ s, coord t ∈ box lo hi) : ‖∑ t ∈ s, SlowFactor.normalizedWeight A B (gridPoint g (coord t)) * a t‖ ≤ 2048 * (6 + 2 * Real.pi) ^ 5 * (1 + V) ^ 5 * coordinatePrefixMax lo hi s coord a

Complete smooth-weight removal on an arbitrary finite carrier. All repeated coordinates, signs, support masks, and arithmetic phases remain in a.

theorem LiLiuPrereqFouvry.Rectangle.norm_coordinate_sum_normalizedWeight_div_le {α : Type u_1} (A B V : ℝ) (hV : |A| + |B| ≤ V) (lo hi : Fin 5 → ℕ) (hbox : ∀ (i : Fin 5), lo i ≤ hi i) (R : Fin 5 → ℝ) (hR : ∀ (i : Fin 5), 0 < R i) (hlo : ∀ (i : Fin 5), R i ≤ ↑(lo i)) (hhi : ∀ (i : Fin 5), ↑(hi i) ≤ 2 * R i) (s : Finset α) (coord : α → Fin 5 → ℕ) (a : α → ℂ) (hcoord : ∀ t ∈ s, coord t ∈ box lo hi) : ‖∑ t ∈ s, (SlowFactor.normalizedWeight A B fun (i : Fin 5) => ↑(coord t i) / R i) * a t‖ ≤ 2048 * (6 + 2 * Real.pi) ^ 5 * (1 + V) ^ 5 * coordinatePrefixMax lo hi s coord a

Dyadic-reference version of complete smooth-weight removal.

theorem LiLiuPrereqFouvry.Rectangle.norm_coordinate_sum_normalizedWeight_div_le_all {α : Type u_1} (A B V : ℝ) (hV : |A| + |B| ≤ V) (lo hi : Fin 5 → ℕ) (R : Fin 5 → ℝ) (hR : ∀ (i : Fin 5), 0 < R i) (hlo : ∀ (i : Fin 5), R i ≤ ↑(lo i)) (hhi : ∀ (i : Fin 5), ↑(hi i) ≤ 2 * R i) (s : Finset α) (coord : α → Fin 5 → ℕ) (a : α → ℂ) (hcoord : ∀ t ∈ s, coord t ∈ box lo hi) : ‖∑ t ∈ s, (SlowFactor.normalizedWeight A B fun (i : Fin 5) => ↑(coord t i) / R i) * a t‖ ≤ 2048 * (6 + 2 * Real.pi) ^ 5 * (1 + V) ^ 5 * coordinatePrefixMax lo hi s coord a

Empty-box-safe finite-carrier version of the concrete weight-removal theorem.