A genuine L² Gevrey product estimate, with the coefficient tensors bounded uniformly and the field tensors measured in L². It applies on any base, including cylinder tensors evaluated through a cover section.

theorem EulerGevreyProductLp.finite_domination {X : Type u_1} {V : Type u_3} [MeasurableSpace X] [NormedAddCommGroup V] {ι : Type u_5} (μ : MeasureTheory.Measure X) (I : Finset ι) (f : X → V) (hf : MeasureTheory.AEStronglyMeasurable f μ) (H : ι → X → ℝ) (hH : ∀ i ∈ I, MeasureTheory.MemLp (H i) 2 μ) (hdom : ∀ (x : X), ‖f x‖ ≤ ∑ i ∈ I, H i x) : MeasureTheory.MemLp f 2 μ ∧ (MeasureTheory.eLpNorm f 2 μ).toReal ≤ ∑ i ∈ I, (MeasureTheory.eLpNorm (H i) 2 μ).toReal

theorem EulerGevreyProductLp.clm_apply_memLp_and_bound {X : Type u_1} {E : Type u_2} {V : Type u_3} {W : Type u_4} [MeasurableSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (μ : MeasureTheory.Measure X) (σ : X → E) (f : E → V →L[ℝ] W) (g : E → V) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (n : ℕ) (hm : MeasureTheory.AEStronglyMeasurable (fun (x : X) => iteratedFDeriv ℝ n (fun (y : E) => (f y) (g y)) (σ x)) μ) (R B C : ℝ) (hR : 0 ≤ R) (hB : 0 ≤ B) (hC : 0 ≤ C) (d e : ℕ) (hb : ∀ j ≤ n, ∀ (x : X), ‖iteratedFDeriv ℝ j f (σ x)‖ ≤ B * EulerGevrey.majorant R d j) (hLp : ∀ j ≤ n, MeasureTheory.MemLp (fun (x : X) => iteratedFDeriv ℝ j g (σ x)) 2 μ) (hNorm : ∀ j ≤ n, (MeasureTheory.eLpNorm (fun (x : X) => iteratedFDeriv ℝ j g (σ x)) 2 μ).toReal ≤ C * EulerGevrey.majorant R e j) : MeasureTheory.MemLp (fun (x : X) => iteratedFDeriv ℝ n (fun (y : E) => (f y) (g y)) (σ x)) 2 μ ∧ (MeasureTheory.eLpNorm (fun (x : X) => iteratedFDeriv ℝ n (fun (y : E) => (f y) (g y)) (σ x)) 2 μ).toReal ≤ 3 * B * C * EulerGevrey.majorant R (d + e) n