English
The coordinates of a σ-linear map between fibers can be expressed via trivializations at x0.
Русский
Координаты σ-линейного отображения между волокнами выражаются через тривиализации в x0.
LaTeX
$$$ inCoordinates F_1 E_1 (F_2 \\to L[\\mathbb{R}] F_3) (fun x => E_2 x \\to L[\\mathbb{R}] E_3 x) x_0 x x_0 x ϕ v w = \\text{...}$$$
Lean4
/-- In a continuous Riemannian bundle, the trivialization at a point is locally bounded in norm. -/
theorem eventually_norm_trivializationAt_lt (x : B) :
∃ C > 0, ∀ᶠ y in 𝓝 x, ‖(trivializationAt F E x).continuousLinearMapAt ℝ y‖ < C :=
by
refine ⟨(1 + ‖(trivializationAt F E x).continuousLinearMapAt ℝ x‖) * 2, by positivity, ?_⟩
filter_upwards [eventually_norm_symmL_trivializationAt_self_comp_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).continuousLinearMapAt ℝ y =
(ContinuousLinearMap.id _ _) ∘L ((trivializationAt F E x).continuousLinearMapAt ℝ y) :=
by simp
grw [this, ← A, comp_assoc, opNorm_comp_le]
gcongr
linarith
