English
In a Riemannian bundle setting, the derivative mfderiv within extChartAt has bounded norm near any point x: there exists C>0 such that eventually the operator norm of mfderiv is less than C along neighbourhoods of x.
Русский
В условиях римманова расслоения можно подобрать константу C>0, чтобы близко к x нормa mfderiv Within была ограничена сверху C.
LaTeX
$$$$\\exists C>0\\;\\forall^\\! y\\in\\mathcal{N}_x,\\; \\|\\mathrm{mfderiv}(I,\\mathcal{I}(\\mathbb{R},E), (extChartAt I x))\, y\\| < C.$$$$
Lean4
theorem eventually_norm_mfderiv_extChartAt_lt (x : M) :
∃ C > 0, ∀ᶠ y in 𝓝 x, ‖mfderiv I 𝓘(ℝ, E) (extChartAt I x) y‖ < C :=
by
rcases eventually_norm_trivializationAt_lt E (fun (x : M) ↦ TangentSpace I x) x with ⟨C, C_pos, hC⟩
refine ⟨C, C_pos, ?_⟩
have hx : (chartAt H x).source ∈ 𝓝 x := chart_source_mem_nhds H x
filter_upwards [hC, hx] with y hy h'y
rwa [← TangentBundle.continuousLinearMapAt_trivializationAt h'y]
