OAI/Geometry/RCD/Coordinates/GevreyExpGlue.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Quantitative flat exponential

The usual flat exponential has Gevrey order two. The proof keeps the factorial-weighted coefficient sum of its derivative polynomials, so that the estimate is uniform on the entire real line.

  1. def OAI.RegularPointCoordinates.gluePolynomial line 20
  2. def OAI.RegularPointCoordinates.coefficientWeight line 24
  3. theorem OAI.RegularPointCoordinates.gluePolynomial_degree line 27
  4. theorem OAI.RegularPointCoordinates.coefficientWeight_shift line 40
  5. theorem OAI.RegularPointCoordinates.coefficientWeight_step line 51
  6. theorem OAI.RegularPointCoordinates.gluePolynomial_weight line 108
  7. theorem OAI.RegularPointCoordinates.gluePolynomial_derivative line 127
  8. theorem OAI.RegularPointCoordinates.norm_iteratedDeriv_expNegInvGlue_le line 138

    Source documentation

    The standard flat exponential is globally Gevrey of order two.

    theorem norm_iteratedDeriv_expNegInvGlue_le (n : ℕ) (x : ℝ) :
    ‖iteratedDeriv n expNegInvGlue x‖ ≤ 8 ^ n * (n.factorial : ℝ) ^ 2 := by
…