The concrete five-variable slow factor, in logarithmic coordinates

The coordinate order is (h,k,n,r,s). Logarithmic coordinates are convenient for dyadic partial summation: their interval lengths are at most log 2, independently of the original arithmetic scales. The two real phase parameters include all scaling constants; arithmetic coefficients and reciprocal/root phases are not part of this weight.

@[reducible, inline]

abbrev LiLiuPrereqFouvry.SlowFactor.Point : Type

Equations

• LiLiuPrereqFouvry.SlowFactor.Point = (Fin 5 → ℝ)

def LiLiuPrereqFouvry.SlowFactor.linear (m x : Point) : ℝ

Equations

• LiLiuPrereqFouvry.SlowFactor.linear m x = ∑ i : Fin 5, m i * x i

def LiLiuPrereqFouvry.SlowFactor.phaseA : Point

Equations

• LiLiuPrereqFouvry.SlowFactor.phaseA = ![1, -1, 0, -1, -1]

def LiLiuPrereqFouvry.SlowFactor.phaseB : Point

Equations

• LiLiuPrereqFouvry.SlowFactor.phaseB = ![1, -1, -1, -1, -1]

def LiLiuPrereqFouvry.SlowFactor.amplitude : Point

Equations

• LiLiuPrereqFouvry.SlowFactor.amplitude = ![0, -1, 0, -1, -1]

noncomputable def LiLiuPrereqFouvry.SlowFactor.atom (A B : ℝ) (m x : Point) : ℂ

Equations

• LiLiuPrereqFouvry.SlowFactor.atom A B m x = Complex.exp (↑(LiLiuPrereqFouvry.SlowFactor.linear m x) + Complex.I * (2 * ↑Real.pi) * (↑A * ↑(Real.exp (LiLiuPrereqFouvry.SlowFactor.linear LiLiuPrereqFouvry.SlowFactor.phaseA x)) + ↑B * ↑(Real.exp (LiLiuPrereqFouvry.SlowFactor.linear LiLiuPrereqFouvry.SlowFactor.phaseB x))))

noncomputable def LiLiuPrereqFouvry.SlowFactor.weight (A B : ℝ) : Point → ℂ

Equations

• LiLiuPrereqFouvry.SlowFactor.weight A B = LiLiuPrereqFouvry.SlowFactor.atom A B LiLiuPrereqFouvry.SlowFactor.amplitude

noncomputable def LiLiuPrereqFouvry.SlowFactor.coeffA (A : ℝ) (j : Fin 5) : ℂ

Equations

• LiLiuPrereqFouvry.SlowFactor.coeffA A j = Complex.I * (2 * ↑Real.pi) * ↑A * ↑(LiLiuPrereqFouvry.SlowFactor.phaseA j)

noncomputable def LiLiuPrereqFouvry.SlowFactor.coeffB (B : ℝ) (j : Fin 5) : ℂ

Equations

• LiLiuPrereqFouvry.SlowFactor.coeffB B j = Complex.I * (2 * ↑Real.pi) * ↑B * ↑(LiLiuPrereqFouvry.SlowFactor.phaseB j)

theorem LiLiuPrereqFouvry.SlowFactor.linear_add (m p x : Point) : linear (m + p) x = linear m x + linear p x

theorem LiLiuPrereqFouvry.SlowFactor.linear_update (m x : Point) (j : Fin 5) (t : ℝ) : linear m (Function.update x j t) = linear m x + m j * (t - x j)

theorem LiLiuPrereqFouvry.SlowFactor.hasDerivAt_linear (m x : Point) (j : Fin 5) : HasDerivAt (fun (t : ℝ) => linear m (Function.update x j t)) (m j) (x j)

theorem LiLiuPrereqFouvry.SlowFactor.atom_shift (A B : ℝ) (m p x : Point) : atom A B (m + p) x = atom A B m x * ↑(Real.exp (linear p x))

theorem LiLiuPrereqFouvry.SlowFactor.norm_atom (A B : ℝ) (m x : Point) : ‖atom A B m x‖ = Real.exp (linear m x)

theorem LiLiuPrereqFouvry.SlowFactor.hasDerivAt_atom (A B : ℝ) (m x : Point) (j : Fin 5) : HasDerivAt (fun (t : ℝ) => atom A B m (Function.update x j t)) (↑(m j) * atom A B m x + coeffA A j * atom A B (m + phaseA) x + coeffB B j * atom A B (m + phaseB) x) (x j)

def LiLiuPrereqFouvry.SlowFactor.jet (A B : ℝ) : List (Fin 5) → Point → Point → ℂ

Appending an index differentiates once in that coordinate; see hasDerivAt_jet. Repeated indices are allowed, so this covers more than the 32 mixed derivatives with each coordinate used at most once.

Equations

• LiLiuPrereqFouvry.SlowFactor.jet A B [] x✝¹ x✝ = LiLiuPrereqFouvry.SlowFactor.atom A B x✝¹ x✝
• LiLiuPrereqFouvry.SlowFactor.jet A B (j :: js) x✝¹ x✝ = ↑(x✝¹ j) * LiLiuPrereqFouvry.SlowFactor.jet A B js x✝¹ x✝ + LiLiuPrereqFouvry.SlowFactor.coeffA A j * LiLiuPrereqFouvry.SlowFactor.jet A B js (x✝¹ + LiLiuPrereqFouvry.SlowFactor.phaseA) x✝ + LiLiuPrereqFouvry.SlowFactor.coeffB B j * LiLiuPrereqFouvry.SlowFactor.jet A B js (x✝¹ + LiLiuPrereqFouvry.SlowFactor.phaseB) x✝

theorem LiLiuPrereqFouvry.SlowFactor.hasDerivAt_jet (A B : ℝ) (js : List (Fin 5)) (m x : Point) (j : Fin 5) : HasDerivAt (fun (t : ℝ) => jet A B js m (Function.update x j t)) (jet A B (js ++ [j]) m x) (x j)

theorem LiLiuPrereqFouvry.SlowFactor.jet_append_eq_deriv (A B : ℝ) (js : List (Fin 5)) (m x : Point) (j : Fin 5) : jet A B (js ++ [j]) m x = deriv (fun (t : ℝ) => jet A B js m (Function.update x j t)) (x j)

def LiLiuPrereqFouvry.SlowFactor.logBox (x : Point) : Prop

Equations

• LiLiuPrereqFouvry.SlowFactor.logBox x = ∀ (i : Fin 5), 0 ≤ x i ∧ x i ≤ Real.log 2

theorem LiLiuPrereqFouvry.SlowFactor.phaseA_abs_le (j : Fin 5) : |phaseA j| ≤ 1

theorem LiLiuPrereqFouvry.SlowFactor.phaseB_abs_le (j : Fin 5) : |phaseB j| ≤ 1

theorem LiLiuPrereqFouvry.SlowFactor.linear_phaseA_le {x : Point} (hx : logBox x) : linear phaseA x ≤ Real.log 2

theorem LiLiuPrereqFouvry.SlowFactor.linear_phaseB_le {x : Point} (hx : logBox x) : linear phaseB x ≤ Real.log 2

theorem LiLiuPrereqFouvry.SlowFactor.norm_coeffA_le (A : ℝ) (j : Fin 5) : ‖coeffA A j‖ ≤ 2 * Real.pi * |A|

theorem LiLiuPrereqFouvry.SlowFactor.norm_coeffB_le (B : ℝ) (j : Fin 5) : ‖coeffB B j‖ ≤ 2 * Real.pi * |B|

theorem LiLiuPrereqFouvry.SlowFactor.norm_jet_le (A B V : ℝ) (hV : |A| + |B| ≤ V) (js : List (Fin 5)) (m x : Point) (hx : logBox x) (R : ℕ) (hm : ∀ (j : Fin 5), |m j| ≤ ↑R) (hl : linear m x ≤ ↑R * Real.log 2) : ‖jet A B js m x‖ ≤ 2 ^ (R + js.length) * (↑(R + js.length) + 2 * Real.pi * V) ^ js.length

A quantitative estimate for every concrete mixed derivative of every exponential monomial generated by the derivative recurrence. No derivative bound is a hypothesis: the assumptions concern only the initial linear exponent and the two real phase parameters.

theorem LiLiuPrereqFouvry.SlowFactor.norm_weight_jet_le (A B V : ℝ) (hV : |A| + |B| ≤ V) (js : List (Fin 5)) (x : Point) (hx : logBox x) : ‖jet A B js amplitude x‖ ≤ 2 ^ (1 + js.length) * (↑(1 + js.length) + 2 * Real.pi * V) ^ js.length

All mixed derivatives of order n, including repeated-coordinate ones, have an explicit degree-n polynomial loss in the phase size.

theorem LiLiuPrereqFouvry.SlowFactor.norm_weight_jet_le_five (A B V : ℝ) (hV : |A| + |B| ≤ V) (js : List (Fin 5)) (hn : js.length ≤ 5) (x : Point) (hx : logBox x) : ‖jet A B js amplitude x‖ ≤ 64 * (6 + 2 * Real.pi) ^ 5 * (1 + V) ^ 5

A single degree-five loss controls all the derivatives required for five-dimensional partial summation.

noncomputable def LiLiuPrereqFouvry.SlowFactor.normalizedWeight (A B : ℝ) (v : Point) : ℂ

The exact normalized kernel in the original positive variables.

Equations

• LiLiuPrereqFouvry.SlowFactor.normalizedWeight A B v = ↑(v 1 * v 3 * v 4)⁻¹ * Complex.exp (Complex.I * (2 * ↑Real.pi) * ↑(A * v 0 / (v 1 * v 3 * v 4) + B * v 0 / (v 1 * v 2 * v 3 * v 4)))

theorem LiLiuPrereqFouvry.SlowFactor.weight_log_eq_normalizedWeight (A B : ℝ) (v : Point) (hv : ∀ (i : Fin 5), 0 < v i) : (weight A B fun (i : Fin 5) => Real.log (v i)) = normalizedWeight A B v

theorem LiLiuPrereqFouvry.SlowFactor.log_mem_logBox (v : Point) (hv : ∀ (i : Fin 5), 1 ≤ v i ∧ v i ≤ 2) : logBox fun (i : Fin 5) => Real.log (v i)

theorem LiLiuPrereqFouvry.SlowFactor.normalized_log_mixed_bound (A B V : ℝ) (hV : |A| + |B| ≤ V) (js : List (Fin 5)) (hn : js.length ≤ 5) (v : Point) (hv : ∀ (i : Fin 5), 1 ≤ v i ∧ v i ≤ 2) : ‖jet A B js amplitude fun (i : Fin 5) => Real.log (v i)‖ ≤ 64 * (6 + 2 * Real.pi) ^ 5 * (1 + V) ^ 5

Application-ready positive-shell form. These are actual logarithmic mixed derivatives of normalizedWeight; weight_log_eq_normalizedWeight identifies the underlying weight, and hasDerivAt_jet certifies every derivative step.