English
The inner product of two differentiable vector-bundle-valued maps is differentiable when interpreted in local coordinates.
Русский
Скалярное произведение двух гладких карт векторного расслоения дифференцируемо в локальных координатах.
LaTeX
$$$\\text{ContMDiffWithinAt}\\; IM\\; (IB.prod 𝓘(\\mathbb{R},F))\\; n\\ (\\lambda m, v_m)\\; s\\ x_0 \\wedge \\text{ContMDiffWithinAt}\\; IM\\; (IB.prod 𝓘(\\mathbb{R},F))\\; n\\ (\\lambda m, w_m)\\; s\\ x_0 \\Rightarrow \\\\text{ContMDiffWithinAt}\\;IM\\; 𝓘(\\mathbb{R})\\; n\\ (\\lambda m, \\langle v_m, w_m\\rangle)\\; s\\ x_0$$$
Lean4
/-- Given two smooth maps into the same fibers of a Riemannian bundle,
their scalar product is smooth. -/
theorem inner_bundle (hv : ContMDiffWithinAt IM (IB.prod 𝓘(ℝ, F)) n (fun m ↦ (v m : TotalSpace F E)) s x)
(hw : ContMDiffWithinAt IM (IB.prod 𝓘(ℝ, F)) n (fun m ↦ (w m : TotalSpace F E)) s x) :
ContMDiffWithinAt IM 𝓘(ℝ) n (fun m ↦ ⟪v m, w m⟫) s x :=
by
rcases h.exists_contMDiff with ⟨g, g_smooth, hg⟩
have hb : ContMDiffWithinAt IM IB n b s x :=
by
simp only [contMDiffWithinAt_totalSpace] at hv
exact hv.1
simp only [hg]
have :
ContMDiffWithinAt IM (IB.prod 𝓘(ℝ)) n
(fun m ↦ TotalSpace.mk' ℝ (E := Bundle.Trivial B ℝ) (b m) (g (b m) (v m) (w m))) s x :=
by
apply ContMDiffWithinAt.clm_bundle_apply₂ (F₁ := F) (F₂ := F)
· exact ContMDiffAt.comp_contMDiffWithinAt x g_smooth.contMDiffAt hb
· exact hv
· exact hw
simp only [contMDiffWithinAt_totalSpace] at this
exact this.2
