The L² composition estimate over an arbitrary measure space. This version allows the base to be a periodic cylinder while the derivatives are tensors on its Euclidean cover. The output is the literal finite Taylor composition of the given jets.

theorem EulerGevreyJetCompositionLp.taylorComp_partition_bound {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (P : FormalMultilinearSeries ℝ E E) (Q : FormalMultilinearSeries ℝ E F) (n : ℕ) (B R : ℝ) (hP : ∀ (j : ℕ), 0 < j → j ≤ n → ‖P j‖ ≤ B * R ^ j * ↑j.factorial ^ 2) : ‖Q.taylorComp P n‖ ≤ ∑ c : OrderedFinpartition n, EulerGevreyCompositionLp.innerPartitionBound B R c * ‖Q c.length‖

theorem EulerGevreyJetCompositionLp.composition_memLp_and_bound {X : Type u_1} {E : Type u_2} {F : Type u_3} [MeasurableSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (μ : MeasureTheory.Measure X) (φ : X → X) (hφ : MeasureTheory.MeasurePreserving φ μ μ) (P : X → FormalMultilinearSeries ℝ E E) (Q : X → FormalMultilinearSeries ℝ E F) (n : ℕ) (hcomp : MeasureTheory.AEStronglyMeasurable (fun (x : X) => (Q (φ x)).taylorComp (P x) n) μ) (A B R S : ℝ) (hA : 0 ≤ A) (hB : 0 ≤ B) (hR : 0 ≤ R) (hS : 0 ≤ S) (hQLp : ∀ j ≤ n, MeasureTheory.MemLp (fun (x : X) => Q x j) 2 μ) (hQ : ∀ j ≤ n, (MeasureTheory.eLpNorm (fun (x : X) => Q x j) 2 μ).toReal ≤ A * S ^ j * ↑j.factorial ^ 2) (hP : ∀ (j : ℕ), 0 < j → j ≤ n → ∀ (x : X), ‖P x j‖ ≤ B * R ^ j * ↑j.factorial ^ 2) : MeasureTheory.MemLp (fun (x : X) => (Q (φ x)).taylorComp (P x) n) 2 μ ∧ (MeasureTheory.eLpNorm (fun (x : X) => (Q (φ x)).taylorComp (P x) n) 2 μ).toReal ≤ A * (R * (B * S + 2)) ^ n * ↑n.factorial ^ 2

Outer tensors are transported in L² by the actual measure-preserving map; only the positive inner tensors use uniform bounds.