English
At a fixed point m0, if the data above hold locally, then the map m ↦ ϕ_m(v_m) is differentiable at m0.
Русский
В окрестности точки m0, если данные удовлетворяют условиям выше, то отображение m ↦ ϕ_m(v_m) дифференцируемо в точке m0.
LaTeX
$$$MDifferentiableAt IM (IB_1.prod 𝓘(\\mathbb{k},F_1))(m_0)\\; (v)\\; (hb_2) \\Rightarrow\\; MDifferentiableAt IM (IB_2.prod 𝓘(\\mathbb{k},F_2))(m_0)(\\lambda m, ϕ_m(v_m))$$$
Lean4
/-- Consider a differentiable map `v : M → E₁` to a vector bundle, over a basemap `b₁ : M → B₁`, and
another basemap `b₂ : M → B₂`. Given linear maps `ϕ m : E₁ (b₁ m) → E₂ (b₂ m)` depending
differentiably on `m`, one can apply `ϕ m` to `g m`, and the resulting map is differentiable.
Note that the differentiability of `ϕ` cannot be always be stated as differentiability of a map
into a manifold, as the pullback bundles `b₁ *ᵖ E₁` and `b₂ *ᵖ E₂` only make sense when `b₁`
and `b₂` are globally smooth, but we want to apply this lemma with only local information.
Therefore, we formulate it using differentiability of `ϕ` read in coordinates.
Version for `MDifferentiableAt`. We also give a version for `MDifferentiableWithinAt`,
but no version for `MDifferentiableOn` or `MDifferentiable` as our assumption, written
in coordinates, only makes sense around a point.
-/
theorem clm_apply_of_inCoordinates
(hϕ :
MDifferentiableAt IM 𝓘(𝕜, F₁ →L[𝕜] F₂) (fun m ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) m₀)
(hv : MDifferentiableAt IM (IB₁.prod 𝓘(𝕜, F₁)) (fun m ↦ (v m : TotalSpace F₁ E₁)) m₀)
(hb₂ : MDifferentiableAt IM IB₂ b₂ m₀) :
MDifferentiableAt IM (IB₂.prod 𝓘(𝕜, F₂)) (fun m ↦ (ϕ m (v m) : TotalSpace F₂ E₂)) m₀ :=
by
rw [← mdifferentiableWithinAt_univ] at hϕ hv hb₂ ⊢
exact MDifferentiableWithinAt.clm_apply_of_inCoordinates hϕ hv hb₂
