English
The inner product of two differentiable maps into a Riemannian bundle is differentiable within at a point, with coordinate readout.
Русский
Скалярное произведение двух дифференцируемых в окрестности отображений в терминах координат дифференцируемо в точке.
LaTeX
$$MDifferentiableWithinAt IM (IB.prod 𝓘(ℝ,F)) n (λ m, ⟪v m, w m⟫) s m0$$
Lean4
/-- Given two differentiable maps into the same fibers of a Riemannian bundle,
their scalar product is differentiable. -/
theorem inner_bundle (hv : MDifferentiableWithinAt IM (IB.prod 𝓘(ℝ, F)) (fun m ↦ (v m : TotalSpace F E)) s x)
(hw : MDifferentiableWithinAt IM (IB.prod 𝓘(ℝ, F)) (fun m ↦ (w m : TotalSpace F E)) s x) :
MDifferentiableWithinAt IM 𝓘(ℝ) (fun m ↦ ⟪v m, w m⟫) s x :=
by
rcases h.exists_contMDiff with ⟨g, g_smooth, hg⟩
have hb : MDifferentiableWithinAt IM IB b s x :=
by
simp only [mdifferentiableWithinAt_totalSpace] at hv
exact hv.1
simp only [hg]
have :
MDifferentiableWithinAt IM (IB.prod 𝓘(ℝ))
(fun m ↦ TotalSpace.mk' ℝ (E := Bundle.Trivial B ℝ) (b m) (g (b m) (v m) (w m))) s x :=
by
apply MDifferentiableWithinAt.clm_bundle_apply₂ (F₁ := F) (F₂ := F)
· exact MDifferentiableAt.comp_mdifferentiableWithinAt x (g_smooth.mdifferentiableAt le_rfl) hb
· exact hv
· exact hw
simp only [mdifferentiableWithinAt_totalSpace] at this
exact this.2
