Mixed rectangular increments of the actual slow weight

Each increment costs its side length, not the number of sampled points. Consequently subdivision of any side does not increase the sum of these bounds. This is the local analytic estimate used by rectangular summation.

def LiLiuPrereqFouvry.SlowFactor.boxDiff : List (Fin 5) → Point → Point → (Point → ℂ) → Point → ℂ

Equations

• LiLiuPrereqFouvry.SlowFactor.boxDiff [] x✝³ x✝² x✝¹ x✝ = x✝¹ x✝
• LiLiuPrereqFouvry.SlowFactor.boxDiff (j :: js) x✝³ x✝² x✝¹ x✝ = LiLiuPrereqFouvry.SlowFactor.boxDiff js x✝³ x✝² x✝¹ (Function.update x✝ j (x✝² j)) - LiLiuPrereqFouvry.SlowFactor.boxDiff js x✝³ x✝² x✝¹ (Function.update x✝ j (x✝³ j))

def LiLiuPrereqFouvry.SlowFactor.sideProduct (js : List (Fin 5)) (lo hi : Point) : ℝ

Equations

• LiLiuPrereqFouvry.SlowFactor.sideProduct js lo hi = (List.map (fun (i : Fin 5) => hi i - lo i) js).prod

theorem LiLiuPrereqFouvry.SlowFactor.hasDerivAt_boxDiff (A B : ℝ) (ds js : List (Fin 5)) (lo hi x : Point) (j : Fin 5) (hjd : j ∉ ds) (hjj : j ∉ js) (hxj : x j ≠ 0) : HasDerivAt (fun (t : ℝ) => boxDiff js lo hi (normalizedJet A B ds) (Function.update x j t)) (boxDiff js lo hi (normalizedJet A B (ds ++ [j])) x) (x j)

theorem LiLiuPrereqFouvry.SlowFactor.shell_update (x : Point) (hx : ∀ (i : Fin 5), 1 ≤ x i ∧ x i ≤ 2) (j : Fin 5) (t : ℝ) (ht : 1 ≤ t ∧ t ≤ 2) (i : Fin 5) : 1 ≤ Function.update x j t i ∧ Function.update x j t i ≤ 2

theorem LiLiuPrereqFouvry.SlowFactor.norm_boxDiff_normalizedJet_le (A B V : ℝ) (hV : |A| + |B| ≤ V) (ds js : List (Fin 5)) (hnd : (ds ++ js).Nodup) (lo hi x : Point) (hlohi : ∀ (i : Fin 5), 1 ≤ lo i ∧ lo i ≤ hi i ∧ hi i ≤ 2) (hx : ∀ (i : Fin 5), 1 ≤ x i ∧ x i ≤ 2) : ‖boxDiff js lo hi (normalizedJet A B ds) x‖ ≤ 64 * (6 + 2 * Real.pi) ^ 5 * (1 + V) ^ 5 * sideProduct js lo hi

An explicit mixed-increment bound for every derivative still needed in the repeated mean-value argument. All analytic hypotheses are proved by the concrete calculus in the two preceding modules.

theorem LiLiuPrereqFouvry.SlowFactor.boxDiff_normalizedJet_nil (A B : ℝ) (js : List (Fin 5)) (lo hi x : Point) (hlo : ∀ (i : Fin 5), 0 < lo i) (hhi : ∀ (i : Fin 5), 0 < hi i) (hx : ∀ (i : Fin 5), 0 < x i) : boxDiff js lo hi (normalizedJet A B []) x = boxDiff js lo hi (normalizedWeight A B) x

theorem LiLiuPrereqFouvry.SlowFactor.norm_boxDiff_normalizedWeight_le (A B V : ℝ) (hV : |A| + |B| ≤ V) (js : List (Fin 5)) (hjs : js.Nodup) (lo hi x : Point) (hlohi : ∀ (i : Fin 5), 1 ≤ lo i ∧ lo i ≤ hi i ∧ hi i ≤ 2) (hx : ∀ (i : Fin 5), 1 ≤ x i ∧ x i ≤ 2) : ‖boxDiff js lo hi (normalizedWeight A B) x‖ ≤ 64 * (6 + 2 * Real.pi) ^ 5 * (1 + V) ^ 5 * sideProduct js lo hi

Concrete rectangular increment estimate, with a product of side lengths. There is no interval-cardinality loss and no assumed variation bound.