Gevrey-two composition with the outer derivatives in actual L². Only the inner positive derivatives are bounded in sup norm. The outer L² norm is transported by a measure-preserving map, so it is not replaced by a pointwise bound or by a volume of the ambient domain.

def EulerGevreyCompositionLp.innerPartitionBound {n : ℕ} (B R : ℝ) (c : OrderedFinpartition n) : ℝ

Inner partition bound, given by ∏ i, B*R^(c.partSize i)*((c.partSize i).factorial : ℝ)^2.

Equations

• EulerGevreyCompositionLp.innerPartitionBound B R c = ∏ i : Fin c.length, B * R ^ c.partSize i * ↑(c.partSize i).factorial ^ 2

theorem EulerGevreyCompositionLp.innerPartitionBound_nonneg {n : ℕ} (B R : ℝ) (hB : 0 ≤ B) (hR : 0 ≤ R) (c : OrderedFinpartition n) : 0 ≤ innerPartitionBound B R c

theorem EulerGevreyCompositionLp.composition_partition_bound {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E → E) (g : E → F) (n : ℕ) (x : E) (hf : ContDiffAt ℝ (↑n) f x) (hg : ContDiffAt ℝ (↑n) g (f x)) (B R : ℝ) (_hB : 0 ≤ B) (_hR : 0 ≤ R) (hfjet : ∀ (j : ℕ), 0 < j → j ≤ n → ‖iteratedFDeriv ℝ j f x‖ ≤ B * R ^ j * ↑j.factorial ^ 2) : ‖iteratedFDeriv ℝ n (g ∘ f) x‖ ≤ ∑ c : OrderedFinpartition n, innerPartitionBound B R c * ‖iteratedFDeriv ℝ c.length g (f x)‖

theorem EulerGevreyCompositionLp.composition_memLp_and_bound {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace E] (μ : MeasureTheory.Measure E) (f : E → E) (g : E → F) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (hmp : MeasureTheory.MeasurePreserving f μ μ) (n : ℕ) (hfg : MeasureTheory.AEStronglyMeasurable (iteratedFDeriv ℝ n (g ∘ f)) μ) (A B R S : ℝ) (hA : 0 ≤ A) (hB : 0 ≤ B) (hR : 0 ≤ R) (hS : 0 ≤ S) (hgLp : ∀ j ≤ n, MeasureTheory.MemLp (iteratedFDeriv ℝ j g) 2 μ) (hgjet : ∀ j ≤ n, (MeasureTheory.eLpNorm (iteratedFDeriv ℝ j g) 2 μ).toReal ≤ A * S ^ j * ↑j.factorial ^ 2) (hfjet : ∀ (j : ℕ), 0 < j → j ≤ n → ∀ (x : E), ‖iteratedFDeriv ℝ j f x‖ ≤ B * R ^ j * ↑j.factorial ^ 2) : MeasureTheory.MemLp (iteratedFDeriv ℝ n (g ∘ f)) 2 μ ∧ (MeasureTheory.eLpNorm (iteratedFDeriv ℝ n (g ∘ f)) 2 μ).toReal ≤ A * (R * (B * S + 2)) ^ n * ↑n.factorial ^ 2

A genuine L² composition estimate with factorial-square growth. The measurability premise is automatic for smooth finite-dimensional fields, and no L² premise is required for the composed derivative.