The multi-index Leibniz rule for multiPartial

The single-axis Leibniz rule for iterated axisDeriv, its three-axis expansion of ∂^α (g h) on a time slice, and the resulting bound |∂^α (g h)| ≤ ∑ₘ C(|α|, m) G m H (|α| - m). This product estimate carries the factorial bookkeeping of the nonlinear and pressure terms in the proof of thm:analytic:interior.

theorem CIV.contDiffOn_axisDeriv_iterate {G : CKN.Foundation.Parabolic.Vec3 → ℝ} {s : Set CKN.Foundation.Parabolic.Vec3} (hs : IsOpen s) (hG : ContDiffOn ℝ (↑⊤) G s) (j : Fin 3) (k : ℕ) : ContDiffOn ℝ (↑⊤) ((axisDeriv j)^[k] G) s

Iterated axis derivatives of a smooth function are smooth.

theorem CIV.axisDeriv_iterate_mul_eqOn_antidiagonal {G H : CKN.Foundation.Parabolic.Vec3 → ℝ} {s : Set CKN.Foundation.Parabolic.Vec3} (hs : IsOpen s) (hG : ContDiffOn ℝ (↑⊤) G s) (hH : ContDiffOn ℝ (↑⊤) H s) (j : Fin 3) (n : ℕ) : Set.EqOn ((axisDeriv j)^[n] fun (y : CKN.Foundation.Parabolic.Vec3) => G y * H y) (fun (y : CKN.Foundation.Parabolic.Vec3) => ∑ ij ∈ Finset.antidiagonal n, ↑(n.choose ij.1) * ((axisDeriv j)^[ij.1] G y * (axisDeriv j)^[ij.2] H y)) s

Single-axis Leibniz rule on an open set, indexed by the antidiagonal.

theorem CIV.axisDeriv_iterate_mul_eqOn {G H : CKN.Foundation.Parabolic.Vec3 → ℝ} {s : Set CKN.Foundation.Parabolic.Vec3} (hs : IsOpen s) (hG : ContDiffOn ℝ (↑⊤) G s) (hH : ContDiffOn ℝ (↑⊤) H s) (j : Fin 3) (n : ℕ) : Set.EqOn ((axisDeriv j)^[n] fun (y : CKN.Foundation.Parabolic.Vec3) => G y * H y) (fun (y : CKN.Foundation.Parabolic.Vec3) => ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ((axisDeriv j)^[i] G y * (axisDeriv j)^[n - i] H y)) s

Single-axis Leibniz rule on an open set.

theorem CIV.axisDeriv_iterate_congr_on {F F' : CKN.Foundation.Parabolic.Vec3 → ℝ} {s : Set CKN.Foundation.Parabolic.Vec3} (hs : IsOpen s) (h : Set.EqOn F F' s) (j : Fin 3) (n : ℕ) : Set.EqOn ((axisDeriv j)^[n] F) ((axisDeriv j)^[n] F') s

Iterated axisDeriv respects agreement on an open set.

theorem CIV.axisDeriv_iterate_finset_sum_eqOn {ι : Type u_1} (u : Finset ι) {F : ι → CKN.Foundation.Parabolic.Vec3 → ℝ} (c : ι → ℝ) {s : Set CKN.Foundation.Parabolic.Vec3} (hs : IsOpen s) (hF : ∀ (k : ι), ContDiffOn ℝ (↑⊤) (F k) s) (j : Fin 3) (n : ℕ) : Set.EqOn ((axisDeriv j)^[n] fun (y : CKN.Foundation.Parabolic.Vec3) => ∑ k ∈ u, c k * F k y) (fun (y : CKN.Foundation.Parabolic.Vec3) => ∑ k ∈ u, c k * (axisDeriv j)^[n] (F k) y) s

Iterated axisDeriv is linear over finite sums of smooth functions on an open set.

theorem CIV.multiPartial_mul_expand {g h : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {Ω : Set CKN.Foundation.Parabolic.Vec3} (hΩ : IsOpen Ω) (t : ℝ) (hg : ContDiffOn ℝ (↑⊤) (fun (x : CKN.Foundation.Parabolic.Vec3) => g (x, t)) Ω) (hh : ContDiffOn ℝ (↑⊤) (fun (x : CKN.Foundation.Parabolic.Vec3) => h (x, t)) Ω) {x : CKN.Foundation.Parabolic.Vec3} (hx : x ∈ Ω) (α : Fin 3 → ℕ) : multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => g w * h w) α (x, t) = ∑ a ∈ Finset.range (α 0 + 1), ∑ b ∈ Finset.range (α 1 + 1), ∑ c ∈ Finset.range (α 2 + 1), ↑((α 0).choose a) * ↑((α 1).choose b) * ↑((α 2).choose c) * (multiPartial g ![a, b, c] (x, t) * multiPartial h ![α 0 - a, α 1 - b, α 2 - c] (x, t))

Three-axis Leibniz expansion of ∂^α (g h) on a time slice.

theorem CIV.abs_multiPartial_mul_le {g h : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {Ω : Set CKN.Foundation.Parabolic.Vec3} (hΩ : IsOpen Ω) (t : ℝ) (hg : ContDiffOn ℝ (↑⊤) (fun (x : CKN.Foundation.Parabolic.Vec3) => g (x, t)) Ω) (hh : ContDiffOn ℝ (↑⊤) (fun (x : CKN.Foundation.Parabolic.Vec3) => h (x, t)) Ω) {x : CKN.Foundation.Parabolic.Vec3} (hx : x ∈ Ω) (α : Fin 3 → ℕ) (G H : ℕ → ℝ) (hG : ∀ (γ : Fin 3 → ℕ), (∀ (i : Fin 3), γ i ≤ α i) → |multiPartial g γ (x, t)| ≤ G (γ 0 + γ 1 + γ 2)) (hH : ∀ (γ : Fin 3 → ℕ), (∀ (i : Fin 3), γ i ≤ α i) → |multiPartial h γ (x, t)| ≤ H (γ 0 + γ 1 + γ 2)) : |multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => g w * h w) α (x, t)| ≤ ∑ m ∈ Finset.range (α 0 + α 1 + α 2 + 1), ↑((α 0 + α 1 + α 2).choose m) * (G m * H (α 0 + α 1 + α 2 - m))

The multi-index Leibniz bound: with bounds G m, H m on the derivatives of order m ≤ |α|, |∂^α (g h)| ≤ ∑ₘ C(|α|, m) G m H (|α| - m).