English
Differentiability of two bundle-valued maps implies differentiability of their fiberwise inner product.
Русский
Дифференцируемость двух отображений в расслоении влечёт дифференцируемость их волокно-производного внутр. произведения.
LaTeX
$$MDifferentiableWithinAt IM (IB.prod 𝓘(ℝ,F)) n (λ m, v_m) ∧ MDifferentiableWithinAt IM (IB.prod 𝓘(ℝ,F)) n (λ m, w_m) ⇒ ContMDiffWithinAt IM (𝓘(ℝ)) 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 : MDifferentiable IM (IB.prod 𝓘(ℝ, F)) (fun m ↦ (v m : TotalSpace F E)))
(hw : MDifferentiable IM (IB.prod 𝓘(ℝ, F)) (fun m ↦ (w m : TotalSpace F E))) :
MDifferentiable IM 𝓘(ℝ) (fun b ↦ ⟪v b, w b⟫) := fun x ↦ (hv x).inner_bundle (hw x)
