Quantitative calculus for concrete smooth L² fields, with the outer factor in L² and the inner coordinate change preserving volume.

def EulerGevrey.HasSupBound {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (f : E → V) (C R : ℝ) : Prop

Has sup bound, given by ∀ n x, ‖iteratedFDeriv ℝ n f x‖ ≤ C*R^n*(n.factorial : ℝ)^2.

Equations

• EulerGevrey.HasSupBound f C R = ∀ (n : ℕ) (x : E), ‖iteratedFDeriv ℝ n f x‖ ≤ C * R ^ n * ↑n.factorial ^ 2

theorem EulerGevrey.HasSupBound.mono {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {f : E → V} {C R D S : ℝ} (h : HasSupBound f C R) (hC : 0 ≤ C) (hR : 0 ≤ R) (hCD : C ≤ D) (hRS : R ≤ S) : HasSupBound f D S

theorem EulerGevrey.HasSupBound.derivative {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {f : E → V} {C R : ℝ} (h : HasSupBound f C R) (hC : 0 ≤ C) (hR : 0 ≤ R) : HasSupBound (fderiv ℝ f) (C * R) (4 * R)

theorem EulerGevrey.HasSupBound.comp {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {f : E → E} {g : E → V} {C B R S : ℝ} (hg : HasSupBound g C S) (hf : ContDiff ℝ (↑⊤) f) (hgsm : ContDiff ℝ (↑⊤) g) (hC : 0 ≤ C) (hB : 0 ≤ B) (hR : 0 ≤ R) (hS : 0 ≤ S) (hfb : ∀ (n : ℕ), 0 < n → ∀ (x : E), ‖iteratedFDeriv ℝ n f x‖ ≤ B * R ^ n * ↑n.factorial ^ 2) : HasSupBound (g ∘ f) C (R * (B * S + 2))

theorem EulerGevrey.HasSupBound.apply {E : Type u_1} {V : Type u_2} {W : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {f : E → V →L[ℝ] W} {g : E → V} {B C R : ℝ} (hf : HasSupBound f B R) (hg : HasSupBound g C R) (hfsm : ContDiff ℝ (↑⊤) f) (hgsm : ContDiff ℝ (↑⊤) g) (hB : 0 ≤ B) (hC : 0 ≤ C) (hR : 0 ≤ R) : HasSupBound (fun (x : E) => (f x) (g x)) (3 * B * C) R

theorem EulerGevrey.positive_id_add_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → E) (hf : ContDiff ℝ (↑⊤) f) (B R : ℝ) (hB : 0 ≤ B) (hR : 0 ≤ R) (hb : HasSupBound f B R) (n : ℕ) (hn : 0 < n) (x : E) : ‖iteratedFDeriv ℝ n (fun (y : E) => y + f y) x‖ ≤ (1 + B) * (1 + R) ^ n * ↑n.factorial ^ 2

theorem EulerLpTranslation.SmoothL2Field.compose_memLp_and_bound {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hf : ContDiff ℝ (↑⊤) f) (hmp : MeasureTheory.MeasurePreserving f MeasureTheory.volume MeasureTheory.volume) (B R : ℝ) (hB : 0 ≤ B) (hR : 0 ≤ R) (hfb : ∀ (n : ℕ), 0 < n → ∀ (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n f x‖ ≤ B * R ^ n * ↑n.factorial ^ 2) (A : SmoothL2Field V) (C S : ℝ) (hC : 0 ≤ C) (hS : 0 ≤ S) (ha : A.HasJetBound C S) (n : ℕ) : MeasureTheory.MemLp (iteratedFDeriv ℝ n (A.field ∘ f)) 2 MeasureTheory.volume ∧ (MeasureTheory.eLpNorm (iteratedFDeriv ℝ n (A.field ∘ f)) 2 MeasureTheory.volume).toReal ≤ C * (R * (B * S + 2)) ^ n * ↑n.factorial ^ 2

def EulerLpTranslation.SmoothL2Field.composeField {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hf : ContDiff ℝ (↑⊤) f) (hmp : MeasureTheory.MeasurePreserving f MeasureTheory.volume MeasureTheory.volume) (B R : ℝ) (hB : 0 ≤ B) (hR : 0 ≤ R) (hfb : ∀ (n : ℕ), 0 < n → ∀ (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n f x‖ ≤ B * R ^ n * ↑n.factorial ^ 2) (A : SmoothL2Field V) (C S : ℝ) (hC : 0 ≤ C) (hS : 0 ≤ S) (ha : A.HasJetBound C S) : SmoothL2Field V

Compose field, bundling field, smooth, integrable.

Equations

• EulerLpTranslation.SmoothL2Field.composeField f hf hmp B R hB hR hfb A C S hC hS ha = { field := A.field ∘ f, smooth := ⋯, integrable := ⋯ }

theorem EulerLpTranslation.SmoothL2Field.composeField_bound {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hf : ContDiff ℝ (↑⊤) f) (hmp : MeasureTheory.MeasurePreserving f MeasureTheory.volume MeasureTheory.volume) (B R : ℝ) (hB : 0 ≤ B) (hR : 0 ≤ R) (hfb : ∀ (n : ℕ), 0 < n → ∀ (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n f x‖ ≤ B * R ^ n * ↑n.factorial ^ 2) (A : SmoothL2Field V) (C S : ℝ) (hC : 0 ≤ C) (hS : 0 ≤ S) (ha : A.HasJetBound C S) : (composeField f hf hmp B R hB hR hfb A C S hC hS ha).HasJetBound C (R * (B * S + 2))

def EulerLpTranslation.SmoothL2Field.productField {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (g : EulerSmoothLimit.Space → V →L[ℝ] W) (hg : ContDiff ℝ (↑⊤) g) (A : SmoothL2Field V) (B C R : ℝ) (hB : 0 ≤ B) (hC : 0 ≤ C) (hR : 0 ≤ R) (hgb : EulerGevrey.HasSupBound g B R) (hab : A.HasJetBound C R) : SmoothL2Field W

Product field, bundling field, smooth, integrable.

Equations

• EulerLpTranslation.SmoothL2Field.productField g hg A B C R hB hC hR hgb hab = { field := fun (x : EulerSmoothLimit.Space) => (g x) (A.field x), smooth := ⋯, integrable := ⋯ }

theorem EulerLpTranslation.SmoothL2Field.productField_bound {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (g : EulerSmoothLimit.Space → V →L[ℝ] W) (hg : ContDiff ℝ (↑⊤) g) (A : SmoothL2Field V) (B C R : ℝ) (hB : 0 ≤ B) (hC : 0 ≤ C) (hR : 0 ≤ R) (hgb : EulerGevrey.HasSupBound g B R) (hab : A.HasJetBound C R) : (productField g hg A B C R hB hC hR hgb hab).HasJetBound (3 * B * C) R