eventually_enorm_mfderiv_extChartAt_lt

English

A symmetric extension chart at x yields bounded derivative; the derivative of the symmetric map has bounded norm near x.

Русский

Симметрическая выпуклая карта extChartAt в точке x даёт ограниченность норм производной симметризированной карты около x.

LaTeX

$$$$\\exists C>0\\;\\forall^\\! y\\in\\mathcal{N}_x,\\; \\|\\mathrm{mfderivWithin}(I,\\text{extChartAt}(I,x).symm, (range I))\\,(y)\\| < C.$$$$

Lean4

theorem eventually_enorm_mfderiv_extChartAt_lt (x : M) :
    ∃ C > (0 : ℝ≥0), ∀ᶠ y in 𝓝 x, ‖mfderiv I 𝓘(ℝ, E) (extChartAt I x) y‖ₑ < C :=
  by
  rcases eventually_norm_mfderiv_extChartAt_lt I x with ⟨C, C_pos, hC⟩
  lift C to ℝ≥0 using C_pos.le
  simp only [gt_iff_lt, NNReal.coe_pos] at C_pos
  refine ⟨C, C_pos, ?_⟩
  filter_upwards [hC] with y hy
  simp only [enorm, nnnorm]
  exact_mod_cast hy

Похожие утверждения