Finite scalar products: bounded coefficient jets times averaged positive T jets. Every differentiation allocation retains its multiplicity.

def AVenhance.Infra.Section5.slowWordSplits : List (Fin 2) → List (List (Fin 2) × List (Fin 2))

Allocations of derivative positions between two scalar factors.

Equations

• One or more equations did not get rendered due to their size.
• AVenhance.Infra.Section5.slowWordSplits [] = [([], [])]

theorem AVenhance.Infra.Section5.slowWordSplits_length (w : List (Fin 2)) : (slowWordSplits w).length = 2 ^ w.length

theorem AVenhance.Infra.Section5.slowWordSplits_sizes (w : List (Fin 2)) (p : List (Fin 2) × List (Fin 2)) (hp : p ∈ slowWordSplits w) : p.1.length + p.2.length = w.length

theorem AVenhance.Infra.Section5.amnrSpaceWord_eq_directionalJet (w : List (Fin 2)) (f : Homogenization.Vec 2 → ℝ) : Section4.amnrSpaceWord w f = FaaDiBruno.directionalJet (List.map Homogenization.basisVec w) f

theorem AVenhance.Infra.Section5.slowWordSplits_map_directions (w : List (Fin 2)) : FaaDiBruno.directionalSplits (List.map Homogenization.basisVec w) = List.map (fun (p : List (Fin 2) × List (Fin 2)) => (List.map Homogenization.basisVec p.1, List.map Homogenization.basisVec p.2)) (slowWordSplits w)

theorem AVenhance.Infra.Section5.slowWord_smooth {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (w : List (Fin 2)) : ContDiff ℝ (↑⊤) (Section4.amnrSpaceWord w f)

theorem AVenhance.Infra.Section5.slowWord_mul_expansion {f g : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (w : List (Fin 2)) : Section4.amnrSpaceWord w (f * g) = (List.map (fun (p : List (Fin 2) × List (Fin 2)) => Section4.amnrSpaceWord p.1 f * Section4.amnrSpaceWord p.2 g) (slowWordSplits w)).sum

theorem AVenhance.Infra.Section5.slowFactor_mul_eLpNorm_le {f g : Homogenization.Vec 2 → ℝ} (hf : Continuous f) (hg : Continuous g) {B : ℝ} (hB : 0 ≤ B) (hb : ∀ (x : Homogenization.Vec 2), |f x| ≤ B) (p : ENNReal) (μ : MeasureTheory.Measure (Homogenization.Vec 2)) : MeasureTheory.eLpNorm (f * g) p μ ≤ ENNReal.ofReal B * MeasureTheory.eLpNorm g p μ

L-infinity times Lp, using an actual pointwise bound rather than an assumed product estimate.

theorem AVenhance.Infra.Section5.slowFactor_listSum_eLpNorm_le (L : List (Homogenization.Vec 2 → ℝ)) {p : ENNReal} (hp : 1 ≤ p) (μ : MeasureTheory.Measure (Homogenization.Vec 2)) : MeasureTheory.eLpNorm L.sum p μ ≤ (List.map (fun (f : Homogenization.Vec 2 → ℝ) => MeasureTheory.eLpNorm f p μ) L).sum

theorem AVenhance.Infra.Section5.slowFactor_split_factorial_le (a b : ℕ) : ↑a.factorial * ↑b.factorial ≤ ↑(a + b).factorial

The two allocated factorials never exceed the total factorial.

theorem AVenhance.Infra.Section5.slowFactor_word_mul_eLpNorm_le {f g : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) {F G L : ℝ} (hF : 0 ≤ F) (hG : 0 ≤ G) (hL : 0 ≤ L) {p : ENNReal} (hp : 1 ≤ p) (μ : MeasureTheory.Measure (Homogenization.Vec 2)) (hfb : ∀ (w : List (Fin 2)) (x : Homogenization.Vec 2), |Section4.amnrSpaceWord w f x| ≤ F * ↑w.length.factorial * L ^ w.length) (hgb : ∀ (w : List (Fin 2)), MeasureTheory.eLpNorm (Section4.amnrSpaceWord w g) p μ ≤ ENNReal.ofReal (G * ↑w.length.factorial * L ^ w.length)) (w : List (Fin 2)) : MeasureTheory.eLpNorm (Section4.amnrSpaceWord w (f * g)) p μ ≤ ENNReal.ofReal (F * G * ↑w.length.factorial * (2 * L) ^ w.length)

A binary product consumes no derivative of T of order zero when its averaged factor was already a positive T jet. Iteration handles any fixed finite number of coefficient factors.