Fixed physical Sobolev bounds from the genuine all-order cylinder word bounds. The constants are finite polynomials at each fixed order; the oscillating phase costs only the indicated power of its frequency.

noncomputable def EulerPhysicalL2Scaling.derivativeSum {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (m : ℕ) (f : EulerSmoothLimit.Space → V) : ℝ

Derivative sum, given by ∑ n ∈ range (m+1), lpNorm (iteratedFDeriv ℝ n f) 2 volume.

Equations

• EulerPhysicalL2Scaling.derivativeSum m f = ∑ n ∈ Finset.range (m + 1), MeasureTheory.lpNorm (iteratedFDeriv ℝ n f) 2 MeasureTheory.volume

def EulerPhysicalL2Scaling.jetPolynomial (R : ℝ) (m : ℕ) : ℝ

Jet polynomial, given by ∑ n ∈ range (m+1), R^n*(n.factorial : ℝ)^2.

Equations

• EulerPhysicalL2Scaling.jetPolynomial R m = ∑ n ∈ Finset.range (m + 1), R ^ n * ↑n.factorial ^ 2

theorem EulerPhysicalL2Scaling.jetPolynomial_nonneg (R : ℝ) (hR : 0 ≤ R) (m : ℕ) : 0 ≤ jetPolynomial R m

noncomputable def EulerPhysicalL2Scaling.physicalDerivativeCost (P R C : ℝ) (m : ℕ) : ℝ

Physical derivative cost, given by ∑ n ∈ range (m+1), (4*C)^n*Real.sqrt (2/P+2*P)*jetPolynomial R (n+1).

Equations

• EulerPhysicalL2Scaling.physicalDerivativeCost P R C m = ∑ n ∈ Finset.range (m + 1), (4 * C) ^ n * √(2 / P + 2 * P) * EulerPhysicalL2Scaling.jetPolynomial R (n + 1)

theorem EulerPhysicalL2Scaling.physicalDerivativeCost_nonneg (P R C : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (m : ℕ) : 0 ≤ physicalDerivativeCost P R C m

theorem EulerPacketCylinderField.Field.WordBound.slice_word_le {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} {q d : ℕ} {R A : ℝ} (hG : G.WordBound q R A d) (t : ↑(Set.Icc 0 T)) (n : ℕ) : EulerParameterWordGevrey.wordSum EulerCylinderSobolev.standardDirection (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) (G.path t)) n 0 ≤ A * EulerGevrey.majorant R d n

theorem EulerPacketCylinderField.Field.WordBound.tower_norm_le_polynomial {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} {q : ℕ} {R A : ℝ} (hG : G.WordBound q R A 0) (t : ↑(Set.Icc 0 T)) (s : ℕ) : ‖(G.toFieldTower.realization s) t‖ ≤ A * EulerPhysicalL2Scaling.jetPolynomial R s

theorem EulerPacketCylinderField.Field.raw_graph_tensor_memLp {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (t : ↑(Set.Icc 0 T)) (k : ℝ) (m : EulerSmoothLimit.Space) (n : ℕ) : MeasureTheory.MemLp (iteratedFDeriv ℝ n fun (x : EulerSmoothLimit.Space) => raw (↑t, x, k * inner ℝ m x)) 2 MeasureTheory.volume

theorem EulerPacketCylinderField.Field.WordBound.raw_graph_tensor_lpNorm_le {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} {q : ℕ} {R A : ℝ} (hG : G.WordBound q R A 0) (t : ↑(Set.Icc 0 T)) (k : ℝ) (m : EulerSmoothLimit.Space) (n : ℕ) : MeasureTheory.lpNorm (iteratedFDeriv ℝ n fun (x : EulerSmoothLimit.Space) => raw (↑t, x, k * inner ℝ m x)) 2 MeasureTheory.volume ≤ EulerCylinderPhysicalTensor.frequencyFactor k m ^ n * 4 ^ n * √(2 / P + 2 * P) * (A * EulerPhysicalL2Scaling.jetPolynomial R (n + 1))

theorem EulerPacketCylinderField.Field.WordBound.scaled_graph_derivativeSum_le {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} {q : ℕ} {R A : ℝ} (hG : G.WordBound q R A 0) (hR : 0 ≤ R) (hA : 0 ≤ A) (t : ↑(Set.Icc 0 T)) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (k : ℝ) (m : EulerSmoothLimit.Space) (C K : ℝ) (hC : 0 ≤ C) (hK : 1 ≤ K) (hfrequency : EulerCylinderPhysicalTensor.frequencyFactor k m ≤ C * K) (s : ℕ) : EulerPhysicalL2Scaling.derivativeSum s (EulerPhysicalL2Scaling.scale ell fun (x : EulerSmoothLimit.Space) => raw (↑t, x, k * inner ℝ m x)) ≤ ell⁻¹ ^ s * K ^ s * A * EulerPhysicalL2Scaling.physicalDerivativeCost P R C s