Ordinary mixed derivatives of the concrete normalized slow weight

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

Equations

• LiLiuPrereqFouvry.SlowFactor.mixedDeriv [] x✝ = x✝
• LiLiuPrereqFouvry.SlowFactor.mixedDeriv (j :: js) x✝ = fun (x : LiLiuPrereqFouvry.SlowFactor.Point) => deriv (fun (t : ℝ) => LiLiuPrereqFouvry.SlowFactor.mixedDeriv js x✝ (Function.update x j t)) (x j)

noncomputable def LiLiuPrereqFouvry.SlowFactor.inverseFactors (js : List (Fin 5)) (v : Point) : ℝ

Equations

• LiLiuPrereqFouvry.SlowFactor.inverseFactors js v = (List.map (fun (j : Fin 5) => (v j)⁻¹) js).prod

noncomputable def LiLiuPrereqFouvry.SlowFactor.normalizedJet (A B : ℝ) (js : List (Fin 5)) (v : Point) : ℂ

Equations

• LiLiuPrereqFouvry.SlowFactor.normalizedJet A B js v = ↑(LiLiuPrereqFouvry.SlowFactor.inverseFactors js v) * LiLiuPrereqFouvry.SlowFactor.jet A B js LiLiuPrereqFouvry.SlowFactor.amplitude fun (i : Fin 5) => Real.log (v i)

theorem LiLiuPrereqFouvry.SlowFactor.log_update (v : Point) (j : Fin 5) (t : ℝ) : (fun (i : Fin 5) => Real.log (Function.update v j t i)) = Function.update (fun (i : Fin 5) => Real.log (v i)) j (Real.log t)

theorem LiLiuPrereqFouvry.SlowFactor.inverseFactors_update (js : List (Fin 5)) (v : Point) (j : Fin 5) (hj : j ∉ js) (t : ℝ) : inverseFactors js (Function.update v j t) = inverseFactors js v

theorem LiLiuPrereqFouvry.SlowFactor.inverseFactors_append (js : List (Fin 5)) (v : Point) (j : Fin 5) : inverseFactors (js ++ [j]) v = inverseFactors js v * (v j)⁻¹

theorem LiLiuPrereqFouvry.SlowFactor.normalizedJet_nil (A B : ℝ) (v : Point) (hv : ∀ (i : Fin 5), 0 < v i) : normalizedJet A B [] v = normalizedWeight A B v

theorem LiLiuPrereqFouvry.SlowFactor.hasDerivAt_normalizedJet (A B : ℝ) (js : List (Fin 5)) (v : Point) (j : Fin 5) (hj : j ∉ js) (hv : v j ≠ 0) : HasDerivAt (fun (t : ℝ) => normalizedJet A B js (Function.update v j t)) (normalizedJet A B (js ++ [j]) v) (v j)

Ordinary differentiation in a coordinate not yet used. The reciprocal factors are derived by the chain rule, not assumed as derivative bounds.

theorem LiLiuPrereqFouvry.SlowFactor.positive_update (v : Point) (hv : ∀ (i : Fin 5), 0 < v i) (j : Fin 5) (t : ℝ) (ht : 0 < t) (i : Fin 5) : 0 < Function.update v j t i

theorem LiLiuPrereqFouvry.SlowFactor.mixedDeriv_normalizedWeight (A B : ℝ) (js : List (Fin 5)) (hjs : js.Nodup) (v : Point) (hv : ∀ (i : Fin 5), 0 < v i) : mixedDeriv js (normalizedWeight A B) v = normalizedJet A B js.reverse v

Identification with recursively defined, ordinary coordinate derivatives. Nodup is exactly the condition that each coordinate is differentiated at most once. Reversing the list merely reconciles the two recursion conventions.

theorem LiLiuPrereqFouvry.SlowFactor.abs_inverseFactors_le_one (js : List (Fin 5)) (v : Point) (hv : ∀ (i : Fin 5), 1 ≤ v i) : |inverseFactors js v| ≤ 1

theorem LiLiuPrereqFouvry.SlowFactor.norm_normalizedJet_le_five (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) : ‖normalizedJet A B js v‖ ≤ 64 * (6 + 2 * Real.pi) ^ 5 * (1 + V) ^ 5

theorem LiLiuPrereqFouvry.SlowFactor.norm_mixedDeriv_normalizedWeight_le (A B V : ℝ) (hV : |A| + |B| ≤ V) (js : List (Fin 5)) (hjs : js.Nodup) (v : Point) (hv : ∀ (i : Fin 5), 1 ≤ v i ∧ v i ≤ 2) : ‖mixedDeriv js (normalizedWeight A B) v‖ ≤ 64 * (6 + 2 * Real.pi) ^ 5 * (1 + V) ^ 5

The complete five-variable, order-at-most-one-in-each-coordinate bound for the actual nonseparable normalized weight. The only size assumption is on the two explicit phase parameters.