Ordinary spatial L² tensor bounds imply the actual classical label Sobolev word bounds. The finite Sobolev order contributes only a fixed polynomial amplitude and one fixed enlargement of the radius.

def EulerLpTranslation.SmoothL2Field.HasJetBound {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothL2Field V) (C R : ℝ) : Prop

Has jet bound, given by ∀ n, ‖A.jetLp n‖ ≤ C*R^n*(n.factorial : ℝ)^2.

Equations

• A.HasJetBound C R = ∀ (n : ℕ), ‖A.jetLp n‖ ≤ C * R ^ n * ↑n.factorial ^ 2

theorem EulerLpTranslation.SmoothL2Field.norm_jetLp {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothL2Field V) (n : ℕ) : ‖A.jetLp n‖ = (MeasureTheory.eLpNorm (iteratedFDeriv ℝ n A.field) 2 MeasureTheory.volume).toReal

theorem EulerLpTranslation.SmoothL2Field.hasJetBound_iff {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothL2Field V) (C R : ℝ) : A.HasJetBound C R ↔ ∀ (n : ℕ), (MeasureTheory.eLpNorm (iteratedFDeriv ℝ n A.field) 2 MeasureTheory.volume).toReal ≤ C * R ^ n * ↑n.factorial ^ 2

theorem EulerLpTranslation.SmoothL2Field.HasJetBound.mono {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {A : SmoothL2Field V} {C R D S : ℝ} (h : A.HasJetBound C R) (hC : 0 ≤ C) (hR : 0 ≤ R) (hCD : C ≤ D) (hRS : R ≤ S) : A.HasJetBound D S

theorem EulerLpTranslation.SmoothL2Field.HasJetBound.add {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {A B : SmoothL2Field V} {C D R : ℝ} (hA : A.HasJetBound C R) (hB : B.HasJetBound D R) : (A.addField B).HasJetBound (C + D) R

theorem EulerLpTranslation.SmoothL2Field.classicalBlockSize_of_jet_bound {ι : Type u_2} [Fintype ι] (directions : ι → EulerSmoothLimit.Space) (hd : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (A : SmoothL2Field EulerSmoothLimit.Space) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hb : A.HasJetBound C R) (n : ℕ) : EulerMeanClassicalWordBounds.classicalBlockSize directions q A.toLp ⋯ n ≤ EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q R C * EulerParameterWordGevrey.sobolevCoefficientRadius ι R ^ n * ↑n.factorial ^ 2

theorem EulerLpTranslation.SmoothL2Field.hasLabelBound_of_jet_bound (A : SmoothL2Field EulerSmoothLimit.Space) (C R K : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hb : A.HasJetBound C R) (hamp : EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 3) 6 R C ≤ K) (hrad : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 3) R ≤ K) : EulerPacketParentLabelBounds.HasLabelBound K A