Leibniz splits of ordered spatial derivatives

Every ordered derivative of a scalar product is a finite sum indexed by the assignments of its derivative letters to the two factors. Keeping the assignments as a list retains the binomial multiplicities when some coordinate directions coincide.

def ESS.lpsLeibnizSplits : List (Fin 3) → List (List (Fin 3) × List (Fin 3))

Assign each letter of an ordered derivative word to one of two factors, retaining repeated assignments (eq:lps-Hm-energy).

Equations

• One or more equations did not get rendered due to their size.
• ESS.lpsLeibnizSplits [] = [([], [])]

theorem ESS.lps_leibniz_splits_degree (α : List (Fin 3)) (p : List (Fin 3) × List (Fin 3)) (hp : p ∈ lpsLeibnizSplits α) : p.1.length + p.2.length = α.length

Every split retains the total derivative degree (eq:lps-Hm-energy).

theorem ESS.lps_leibniz_splits_length (α : List (Fin 3)) : (lpsLeibnizSplits α).length = 2 ^ α.length

A word of length n has 2^n Leibniz assignments, counted with multiplicity (eq:lps-Hm-energy).

theorem ESS.lps_leibniz_splits_sum (α : List (Fin 3)) (A B : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ) (x : CKN.Foundation.Parabolic.Vec3) : CKN.sobolevLeibnizFamily α A B x = (List.map (fun (p : List (Fin 3) × List (Fin 3)) => A p.1 x * B p.2 x) (lpsLeibnizSplits α)).sum

The ordered Leibniz family is the sum of products over all derivative assignments (eq:lps-Hm-energy).

theorem ESS.lps_leibniz_integral_bound (α : List (Fin 3)) (A B : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ) (K : ℝ) (hterm : ∀ p ∈ lpsLeibnizSplits α, MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => A p.1 x * B p.2 x) 2 MeasureTheory.volume ∧ ∫ (x : CKN.Foundation.Parabolic.Vec3), (A p.1 x * B p.2 x) ^ 2 ≤ K) : MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.sobolevLeibnizFamily α A B x ^ 2) MeasureTheory.volume ∧ ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.sobolevLeibnizFamily α A B x ^ 2 ≤ ↑(lpsLeibnizSplits α).length ^ 2 * K

A finite bound on every Leibniz term controls the square integral of the full ordered derivative, with its binomial multiplicities (eq:lps-Hm-energy).