FrozenCutoffDerivatives.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Directional cutoff bounds from its actual normalized jets

theorem OAI.RegularPointCoordinates.frozen_cutoff_directional_bound line 17

Source documentation

Undo the frozen affine source in any derivative order.

theorem frozen_cutoff_directional_bound (T : E ≃L[ℝ] E) (phi : E → ℝ)
    (x v : E) {r W : ℝ} (hr : 0 < r) (m : ℕ) (hphi : ContDiffAt ℝ m phi x)
    (hjet : ‖iteratedFDeriv ℝ m (fun z => phi (frozenSource r T x z)) 0‖ ≤ W) :
    r ^ m * ‖iteratedFDeriv ℝ m phi x (fun _ => v)‖ ≤ W * ‖T v‖ ^ m := by
…

Mentions: OAI.RegularPointCoordinates.frozenSource

theorem OAI.RegularPointCoordinates.frozen_cutoff_first_second line 43

Source documentation

The first two orders of one Gevrey estimate supply exactly the directional hypotheses used by the finite patch-field calculus.

theorem frozen_cutoff_first_second (T : E ≃L[ℝ] E) (phi : E → ℝ)
    (x v : E) {r L : ℝ} (hr : 0 < r) (hL : 0 ≤ L) (hphi : ContDiffAt ℝ 2 phi x)
    (hjet : ∀ m : ℕ, ‖iteratedFDeriv ℝ m (fun z => phi (frozenSource r T x z)) 0‖ ≤
      L ^ (m + 1) * (m.factorial : ℝ) ^ 2) :
    |fderiv ℝ phi x v| ≤ (L ^ 2 + 4 * L ^ 3) / r * ‖T v‖ ∧
    |diagonalSecond phi x v| ≤ (L ^ 2 + 4 * L ^ 3) / r ^ 2 * ‖T v‖ ^ 2 := by
…

Mentions: OAI.RegularPointCoordinates.frozenSource, OAI.RegularPointCoordinates.diagonalSecond