JetStep.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Scalar all-order jet step

At Gevrey exponent σ = 2, the factorial weights in an increment leave only the factor (m + 1)^3 relative to the allowed jet size. The next dyadic scale contributes 2 / 2^m. A single small parameter controls every order m ≥ 2. The differential estimates producing the old jet and increment are explicit premises of the scalar theorem below.

theorem OAI.RegularPointCoordinates.cubic_le_eight_mul_two_pow line 21
Source documentation
The polynomial growth is dominated by the dyadic factor, including the largest case at order three.
```
theorem cubic_le_eight_mul_two_pow (m : ℕ) :
    ((m : ℝ) + 1) ^ 3 ≤ 8 * (2 : ℝ) ^ m := by
…
```
theorem OAI.RegularPointCoordinates.dyadic_cubic_le_sixteen line 47
theorem OAI.RegularPointCoordinates.dyadic_jet_factor_le_half line 52

theorem OAI.RegularPointCoordinates.jet_increment_factorization line 61

Source documentation

Cancellation of factorials and the old exponential base.

theorem jet_increment_factorization {B : ℝ} {m : ℕ} (hm : 1 ≤ m) :
    B ^ m * factorialMajorant m * (m.factorial : ℝ) =
      (B * ((m : ℝ) + 1) ^ 3) *
        (B ^ (m - 1) * (m.factorial : ℝ) ^ 3) := by
…

Mentions: OAI.RegularPointCoordinates.factorialMajorant

theorem OAI.RegularPointCoordinates.scalar_jet_step line 76

Source documentation

The all-order scalar jet step with an explicit smallness condition.

theorem scalar_jet_step {B C epsilon old increment : ℝ} {m : ℕ}
    (hB : 0 ≤ B) (hm : 2 ≤ m) (hsmall : epsilon * C * B ≤ 1 / 32)
    (hold : old ≤ B ^ (m - 1) * (m.factorial : ℝ) ^ 3)
    (hincrement : increment ≤ epsilon * C * B ^ m *
      factorialMajorant m * (m.factorial : ℝ)) :
    (2 / (2 : ℝ) ^ m) * (old + increment) ≤
      B ^ (m - 1) * (m.factorial : ℝ) ^ 3 := by
…

Mentions: OAI.RegularPointCoordinates.factorialMajorant

theorem OAI.RegularPointCoordinates.exists_uniform_scalar_jet_step line 116

Source documentation

A positive parameter can be fixed once, after fixing the constants, so that the scalar jet step holds at every positive order above one.

theorem exists_uniform_scalar_jet_step {B C : ℝ} (hB : 0 ≤ B) (hC : 0 ≤ C) :
    ∃ epsilon : ℝ, 0 < epsilon ∧ ∀ (m : ℕ) (old increment : ℝ), 2 ≤ m →
      old ≤ B ^ (m - 1) * (m.factorial : ℝ) ^ 3 →
      increment ≤ epsilon * C * B ^ m * factorialMajorant m * (m.factorial : ℝ) →
      (2 / (2 : ℝ) ^ m) * (old + increment) ≤
        B ^ (m - 1) * (m.factorial : ℝ) ^ 3 := by
…

Mentions: OAI.RegularPointCoordinates.factorialMajorant