English
Let x be a point in the base B. The inverse of the trivialization at x is locally bounded in operator norm. More precisely, there exists C > 0 such that for y sufficiently near x, the operator norm of the inverse trivialization at x (evaluated at y) is less than C.
Русский
Пусть x — точка на базе B. Обратная тривиализация в точке x локально ограничена по норме оператора. Точно: существует C > 0 such that при близких y к x операторная норма обратной тривиализации в x (в точке y) меньше C.
LaTeX
$$$$\exists C>0,\ \forall y\text{ near }x:\ \|T^{\mathrm{symm}}_{x,y}\| < C.$$$$
Lean4
/-- In a continuous Riemannian bundle, the inverse of the trivialization at a point is locally
bounded in norm. -/
theorem eventually_norm_symmL_trivializationAt_lt (x : B) :
∃ C > 0, ∀ᶠ y in 𝓝 x, ‖(trivializationAt F E x).symmL ℝ y‖ < C :=
by
refine ⟨2 * (1 + ‖(trivializationAt F E x).symmL ℝ x‖), by positivity, ?_⟩
filter_upwards [eventually_norm_symmL_trivializationAt_comp_self_lt F E x one_lt_two] with y hy
have A :
((trivializationAt F E x).continuousLinearMapAt ℝ x) ∘L ((trivializationAt F E x).symmL ℝ x) =
ContinuousLinearMap.id _ _ :=
by
ext v
have h'x : x ∈ (trivializationAt F E x).baseSet := FiberBundle.mem_baseSet_trivializationAt' x
simp only [coe_comp', Trivialization.continuousLinearMapAt_apply, Trivialization.symmL_apply, Function.comp_apply,
coe_id', id_eq]
convert ((trivializationAt F E x).continuousLinearEquivAt ℝ _ h'x).apply_symm_apply v
rw [Trivialization.coe_continuousLinearEquivAt_eq _ h'x]
rfl
have : (trivializationAt F E x).symmL ℝ y = ((trivializationAt F E x).symmL ℝ y) ∘L (ContinuousLinearMap.id _ _) := by
simp
grw [this, ← A, ← comp_assoc, opNorm_comp_le]
gcongr
linarith
