Exact weight identities used in the proposed packet's Gevrey estimates (18)--(19). These lemmas do not assert the nonlinear PDE estimates or an Euler blowup theorem.

noncomputable def EulerPacketWeights.weight (ρ : ℝ) (n : ℕ) : ℝ

Factorial weight at radius ρ for the Gevrey-two energy series.

Equations

• EulerPacketWeights.weight ρ n = ρ ^ n / ↑n.factorial ^ 2

theorem EulerPacketWeights.weight_pos {ρ : ℝ} (hρ : 0 < ρ) (n : ℕ) : 0 < weight ρ n

theorem EulerPacketWeights.factorial_cast_ne_zero (n : ℕ) : ↑n.factorial ≠ 0

theorem EulerPacketWeights.choose_add_lower (j l : ℕ) (hl : 1 ≤ l) : j + 1 ≤ (j + l).choose l

The binomial gain that compensates a Gevrey-2 derivative in a non-top commutator.

theorem EulerPacketWeights.shifted_source_ratio (ρ : ℝ) (hρ : ρ ≠ 0) (j l : ℕ) : ↑(j + l + 1) * weight ρ (j + l + 1) * ↑((j + l).choose l) / (weight ρ l * ↑(j + 1) * weight ρ (j + 1)) = 1 / ↑((j + l + 1).choose l)

Equation (18)'s source weight ratio, written without truncated natural subtraction.

theorem EulerPacketWeights.external_commutator_ratio (ρ : ℝ) (hρ : ρ ≠ 0) (j l : ℕ) : weight ρ (j + l) * ↑((j + l).choose l) / (weight ρ l * ↑(j + 1) * weight ρ (j + 1)) = ρ⁻¹ * ↑(j + 1) / ↑((j + l).choose l)

Equation (19)'s external-commutator ratio.

theorem EulerPacketWeights.shifted_source_ratio_le_one (ρ : ℝ) (hρ : ρ ≠ 0) (j l : ℕ) : ↑(j + l + 1) * weight ρ (j + l + 1) * ↑((j + l).choose l) / (weight ρ l * ↑(j + 1) * weight ρ (j + 1)) ≤ 1

The source ratio in (18) is at most one, uniformly in the derivative indices.

theorem EulerPacketWeights.external_commutator_ratio_le (ρ : ℝ) (hρ : 0 < ρ) (j l : ℕ) (hl : 1 ≤ l) : weight ρ (j + l) * ↑((j + l).choose l) / (weight ρ l * ↑(j + 1) * weight ρ (j + 1)) ≤ ρ⁻¹

The non-top ratio in (19) is at most the inverse radius, with no order loss.