Concrete smooth L² fields obtained from the periodic cover, its oscillating graph, a linear projection and the physical label dilation. The resulting bounds apply to the literal derivatives of those fields.

theorem EulerLpTranslation.SmoothL2Field.norm_jetLp_map_le {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (L : V →L[ℝ] W) (A : SmoothL2Field V) (n : ℕ) : ‖(mapField L A).jetLp n‖ ≤ ‖L‖ * ‖A.jetLp n‖

theorem EulerLpTranslation.SmoothL2Field.HasJetBound.map_contracting {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {A : SmoothL2Field V} {C R : ℝ} (h : A.HasJetBound C R) (L : V →L[ℝ] W) (hL : ‖L‖ ≤ 1) : (mapField L A).HasJetBound C R

noncomputable def EulerLpTranslation.SmoothL2Field.scaleField {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (ell : ℝ) (hell : 0 < ell) (A : SmoothL2Field V) : SmoothL2Field V

Scale field, bundling field, smooth, integrable.

Equations

• EulerLpTranslation.SmoothL2Field.scaleField ell hell A = { field := EulerPhysicalL2Scaling.scale ell A.field, smooth := ⋯, integrable := ⋯ }

@[simp]

theorem EulerLpTranslation.SmoothL2Field.scaleField_apply {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (ell : ℝ) (hell : 0 < ell) (A : SmoothL2Field V) (x : EulerSmoothLimit.Space) : (scaleField ell hell A).field x = ell • A.field (ell⁻¹ • x)

theorem EulerLpTranslation.SmoothL2Field.norm_jetLp_scale_le {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (A : SmoothL2Field V) (n : ℕ) : ‖(scaleField ell hell A).jetLp n‖ ≤ ell⁻¹ ^ n * ‖A.jetLp n‖

theorem EulerLpTranslation.SmoothL2Field.HasJetBound.scale {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {A : SmoothL2Field V} {C R : ℝ} (h : A.HasJetBound C R) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) : (scaleField ell hell A).HasJetBound C (ell⁻¹ * R)

theorem EulerLpTranslation.SmoothL2Field.scale_sup_bound {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (f : EulerSmoothLimit.Space → V) (hf : ContDiff ℝ (↑⊤) f) (B R : ℝ) (hb : ∀ (n : ℕ) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n f x‖ ≤ B * R ^ n * ↑n.factorial ^ 2) (n : ℕ) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (EulerPhysicalL2Scaling.scale ell f) x‖ ≤ B * (ell⁻¹ * R) ^ n * ↑n.factorial ^ 2

noncomputable def EulerPhysicalGraphGevrey.graphField {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] (P : ℝ) [Fact (0 < P)] (f : EulerLiftedGradientSpace.LiftTangent → V) (hperiod : ∀ (c : ↥(AddSubgroup.zmultiples P)) (z : EulerLiftedGradientSpace.LiftTangent), f (z.1, ↑c + z.2) = f z) (hf : ContDiff ℝ (↑⊤) f) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hLp : ∀ (n : ℕ), MeasureTheory.MemLp (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P f q n) 2 (EulerLiftedGradientSpace.liftMeasure P)) (hn : ∀ (n : ℕ), (MeasureTheory.eLpNorm (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P f q n) 2 (EulerLiftedGradientSpace.liftMeasure P)).toReal ≤ C * R ^ n * ↑n.factorial ^ 2) : EulerLpTranslation.SmoothL2Field V

Graph field, bundling field, smooth, integrable.

Equations

• EulerPhysicalGraphGevrey.graphField P f hperiod hf k m C R hC hR hLp hn = { field := f ∘ ⇑(EulerGraphPullback.graphMap k m), smooth := ⋯, integrable := ⋯ }

theorem EulerPhysicalGraphGevrey.graphField_bound {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] (P : ℝ) [Fact (0 < P)] (f : EulerLiftedGradientSpace.LiftTangent → V) (hperiod : ∀ (c : ↥(AddSubgroup.zmultiples P)) (z : EulerLiftedGradientSpace.LiftTangent), f (z.1, ↑c + z.2) = f z) (hf : ContDiff ℝ (↑⊤) f) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hLp : ∀ (n : ℕ), MeasureTheory.MemLp (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P f q n) 2 (EulerLiftedGradientSpace.liftMeasure P)) (hn : ∀ (n : ℕ), (MeasureTheory.eLpNorm (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P f q n) 2 (EulerLiftedGradientSpace.liftMeasure P)).toReal ≤ C * R ^ n * ↑n.factorial ^ 2) : (graphField P f hperiod hf k m C R hC hR hLp hn).HasJetBound (√(2 / P + 2 * P) * C * (1 + R)) (4 * R * EulerCylinderGraphGevrey.graphFactor k m)

noncomputable def EulerPhysicalGraphGevrey.physicalField {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup W] [NormedSpace ℝ W] (P : ℝ) [Fact (0 < P)] (f : EulerLiftedGradientSpace.LiftTangent → V) (hperiod : ∀ (c : ↥(AddSubgroup.zmultiples P)) (z : EulerLiftedGradientSpace.LiftTangent), f (z.1, ↑c + z.2) = f z) (hf : ContDiff ℝ (↑⊤) f) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hLp : ∀ (n : ℕ), MeasureTheory.MemLp (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P f q n) 2 (EulerLiftedGradientSpace.liftMeasure P)) (hn : ∀ (n : ℕ), (MeasureTheory.eLpNorm (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P f q n) 2 (EulerLiftedGradientSpace.liftMeasure P)).toReal ≤ C * R ^ n * ↑n.factorial ^ 2) (ell : ℝ) (hell : 0 < ell) (L : V →L[ℝ] W) : EulerLpTranslation.SmoothL2Field W

Physical field, given by scaleField ell hell (mapField L (graphField P f hperiod hf k m C R hC hR hLp hn)).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem EulerPhysicalGraphGevrey.physicalField_apply {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup W] [NormedSpace ℝ W] (P : ℝ) [Fact (0 < P)] (f : EulerLiftedGradientSpace.LiftTangent → V) (hperiod : ∀ (c : ↥(AddSubgroup.zmultiples P)) (z : EulerLiftedGradientSpace.LiftTangent), f (z.1, ↑c + z.2) = f z) (hf : ContDiff ℝ (↑⊤) f) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hLp : ∀ (n : ℕ), MeasureTheory.MemLp (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P f q n) 2 (EulerLiftedGradientSpace.liftMeasure P)) (hn : ∀ (n : ℕ), (MeasureTheory.eLpNorm (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P f q n) 2 (EulerLiftedGradientSpace.liftMeasure P)).toReal ≤ C * R ^ n * ↑n.factorial ^ 2) (ell : ℝ) (hell : 0 < ell) (L : V →L[ℝ] W) (x : EulerLiftedGradientSpace.Vector3) : (physicalField P f hperiod hf k m C R hC hR hLp hn ell hell L).field x = ell • L (f ((EulerGraphPullback.graphMap k m) (ell⁻¹ • x)))

theorem EulerPhysicalGraphGevrey.physicalField_bound {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup W] [NormedSpace ℝ W] (P : ℝ) [Fact (0 < P)] (f : EulerLiftedGradientSpace.LiftTangent → V) (hperiod : ∀ (c : ↥(AddSubgroup.zmultiples P)) (z : EulerLiftedGradientSpace.LiftTangent), f (z.1, ↑c + z.2) = f z) (hf : ContDiff ℝ (↑⊤) f) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hLp : ∀ (n : ℕ), MeasureTheory.MemLp (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P f q n) 2 (EulerLiftedGradientSpace.liftMeasure P)) (hn : ∀ (n : ℕ), (MeasureTheory.eLpNorm (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P f q n) 2 (EulerLiftedGradientSpace.liftMeasure P)).toReal ≤ C * R ^ n * ↑n.factorial ^ 2) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (L : V →L[ℝ] W) (hL : ‖L‖ ≤ 1) : (physicalField P f hperiod hf k m C R hC hR hLp hn ell hell L).HasJetBound (√(2 / P + 2 * P) * C * (1 + R)) (ell⁻¹ * (4 * R * EulerCylinderGraphGevrey.graphFactor k m))

theorem EulerPhysicalGraphGevrey.physicalField_sup_bound {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup W] [NormedSpace ℝ W] (P : ℝ) [Fact (0 < P)] (f : EulerLiftedGradientSpace.LiftTangent → V) (hperiod : ∀ (c : ↥(AddSubgroup.zmultiples P)) (z : EulerLiftedGradientSpace.LiftTangent), f (z.1, ↑c + z.2) = f z) (hf : ContDiff ℝ (↑⊤) f) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hLp : ∀ (n : ℕ), MeasureTheory.MemLp (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P f q n) 2 (EulerLiftedGradientSpace.liftMeasure P)) (hn : ∀ (n : ℕ), (MeasureTheory.eLpNorm (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P f q n) 2 (EulerLiftedGradientSpace.liftMeasure P)).toReal ≤ C * R ^ n * ↑n.factorial ^ 2) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (L : V →L[ℝ] W) (hL : ‖L‖ ≤ 1) (B S : ℝ) (hb : ∀ (n : ℕ) (z : EulerLiftedGradientSpace.LiftTangent), ‖iteratedFDeriv ℝ n f z‖ ≤ B * S ^ n * ↑n.factorial ^ 2) (n : ℕ) (x : EulerLiftedGradientSpace.Vector3) : ‖iteratedFDeriv ℝ n (physicalField P f hperiod hf k m C R hC hR hLp hn ell hell L).field x‖ ≤ B * (ell⁻¹ * (S * EulerCylinderGraphGevrey.graphFactor k m)) ^ n * ↑n.factorial ^ 2