The fixed physical Sobolev order costs a polynomial in the Gevrey radius. Explicit coarse powers leave room for the source exponent C*=10(s+2), including the sum of all three particle-map fields.

def EulerSobolevSourceExponent.fixedCost (q : ℕ) : ℝ

Fixed cost, given by (2 : ℝ)^q*∑ j ∈ range (q+1), (j.factorial : ℝ)^2.

Equations

• EulerSobolevSourceExponent.fixedCost q = 2 ^ q * ∑ j ∈ Finset.range (q + 1), ↑j.factorial ^ 2

theorem EulerSobolevSourceExponent.fixedCost_nonneg (q : ℕ) : 0 ≤ fixedCost q

theorem EulerSobolevSourceExponent.coefficient_radius_le (k R : ℝ) (hk : 12 ≤ k) (hR : R ≤ k ^ 5) : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 3) R ≤ k ^ 6

theorem EulerSobolevSourceExponent.coefficient_amplitude_le (q : ℕ) (k C R : ℝ) (hk : 12 ≤ k) (hcost : fixedCost q ≤ k) (_hC : 0 ≤ C) (hR : 0 ≤ R) (hCb : C ≤ k ^ 6) (hRb : R ≤ k ^ 5) : EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 3) q R C ≤ k ^ (6 * q + 7)

theorem EulerSobolevSourceExponent.source_cost_bounds (q : ℕ) (k C R : ℝ) (hk : 12 ≤ k) (hcost : fixedCost q ≤ k) (hC : 0 ≤ C) (hR : 0 ≤ R) (hCb : C ≤ k ^ 6) (hRb : R ≤ k ^ 5) : 3 * EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 3) q R C ≤ k ^ (10 * (q + 2)) ∧ EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 3) R ≤ k ^ (10 * (q + 2))

theorem EulerSobolevSourceExponent.triple_classical_bound (q : ℕ) (A B C : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (M R J : ℝ) (hM : 0 ≤ M) (hR : 0 ≤ R) (hA : A.HasJetBound M R) (hB : B.HasJetBound M R) (hC : C.HasJetBound M R) (hcost : 3 * EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 3) q R M ≤ J) (hrad : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 3) R ≤ J) (n : ℕ) : EulerMeanClassicalWordBounds.classicalBlockSize EulerPacketParentLabelBounds.direction q A.toLp ⋯ n + EulerMeanClassicalWordBounds.classicalBlockSize EulerPacketParentLabelBounds.direction q B.toLp ⋯ n + EulerMeanClassicalWordBounds.classicalBlockSize EulerPacketParentLabelBounds.direction q C.toLp ⋯ n ≤ J ^ (n + 1) * ↑n.factorial ^ 2

theorem EulerSobolevSourceExponent.source_triple_classical_bound (q : ℕ) (A B C : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (k M R : ℝ) (hk : 12 ≤ k) (hcost : fixedCost q ≤ k) (hM : 0 ≤ M) (hR : 0 ≤ R) (hMb : M ≤ k ^ 6) (hRb : R ≤ k ^ 5) (hA : A.HasJetBound M R) (hB : B.HasJetBound M R) (hC : C.HasJetBound M R) (n : ℕ) : EulerMeanClassicalWordBounds.classicalBlockSize EulerPacketParentLabelBounds.direction q A.toLp ⋯ n + EulerMeanClassicalWordBounds.classicalBlockSize EulerPacketParentLabelBounds.direction q B.toLp ⋯ n + EulerMeanClassicalWordBounds.classicalBlockSize EulerPacketParentLabelBounds.direction q C.toLp ⋯ n ≤ (k ^ (10 * (q + 2))) ^ (n + 1) * ↑n.factorial ^ 2