English
There exists a neighborhood where the operator norm of the trivialization is controlled by a constant.
Русский
Существует окрестность, в которой нормa операторa тривиализации ограничена константой.
LaTeX
$$$\\exists C>0,\\; \\forall y \\text{ near } x, \\; \\| (\\operatorname{trivializationAt} F E x).continuousLinearMapAt \\| < C$$$
Lean4
/-- Consider a continuous map `v : M → E₁` to a vector bundle, over a base map `b₁ : M → B₁`, and
another basemap `b₂ : M → B₂`. Given linear maps `ϕ m : E₁ (b₁ m) → E₂ (b₂ m)` depending
continuously on `m`, one can apply `ϕ m` to `g m`, and the resulting map is continuous.
Note that the continuity of `ϕ` cannot be always be stated as continuity of a map into a bundle,
as the pullback bundles `b₁ *ᵖ E₁` and `b₂ *ᵖ E₂` only have a nice topology when `b₁` and `b₂` are
globally continuous, but we want to apply this lemma with only local information. Therefore, we
formulate it using continuity of `ϕ` read in coordinates.
Version for `ContinuousWithinAt`. We also give a version for `ContinuousAt`, but no version for
`ContinuousOn` or `Continuous` as our assumption, written in coordinates, only makes sense around
a point.
For a version with `B₁ = B₂` and `b₁ = b₂`, in which continuity can be expressed without
`inCoordinates`, see `ContinuousWithinAt.clm_bundle_apply`
-/
theorem clm_apply_of_inCoordinates
(hϕ : ContinuousWithinAt (fun m ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) s m₀)
(hv : ContinuousWithinAt (fun m ↦ (v m : TotalSpace F₁ E₁)) s m₀) (hb₂ : ContinuousWithinAt b₂ s m₀) :
ContinuousWithinAt (fun m ↦ (ϕ m (v m) : TotalSpace F₂ E₂)) s m₀ :=
by
rw [← continuousWithinAt_insert_self] at hϕ hv hb₂ ⊢
rw [FiberBundle.continuousWithinAt_totalSpace] at hv ⊢
refine ⟨hb₂, ?_⟩
apply (ContinuousWithinAt.clm_apply hϕ hv.2).congr_of_eventuallyEq_of_mem ?_ (mem_insert m₀ s)
have A : ∀ᶠ m in 𝓝[insert m₀ s] m₀, b₁ m ∈ (trivializationAt F₁ E₁ (b₁ m₀)).baseSet :=
by
apply hv.1
apply (trivializationAt F₁ E₁ (b₁ m₀)).open_baseSet.mem_nhds
exact FiberBundle.mem_baseSet_trivializationAt' (b₁ m₀)
have A' : ∀ᶠ m in 𝓝[insert m₀ s] m₀, b₂ m ∈ (trivializationAt F₂ E₂ (b₂ m₀)).baseSet :=
by
apply hb₂
apply (trivializationAt F₂ E₂ (b₂ m₀)).open_baseSet.mem_nhds
exact FiberBundle.mem_baseSet_trivializationAt' (b₂ m₀)
filter_upwards [A, A'] with m hm h'm
simp [inCoordinates_eq hm h'm, Trivialization.symm_apply_apply_mk (trivializationAt F₁ E₁ (b₁ m₀)) hm (v m)]
