Generalization of calculus results to InnerProductSpace'

noncomputable def fderivInnerCLM' {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [InnerProductSpace' ℝ E] (p : E × E) : E × E →L[ℝ] ℝ

Derivative of the inner product for the instance InnerProductSpace'.

Equations

• fderivInnerCLM' p = ⋯.deriv p

theorem HasFDerivAt.inner' {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [InnerProductSpace' ℝ F] {x : E} {f g : E → F} {f' g' : E →L[ℝ] F} (hf : HasFDerivAt f f' x) (hg : HasFDerivAt g g' x) : HasFDerivAt (fun (t : E) => Inner.inner ℝ (f t) (g t)) ((fderivInnerCLM' (f x, g x)).comp (f'.prod g')) x

theorem fderiv_inner_apply' {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [InnerProductSpace' ℝ F] {f g : E → F} {x : E} (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) (y : E) : (fderiv ℝ (fun (t : E) => inner ℝ (f t) (g t)) x) y = inner ℝ (f x) ((fderiv ℝ g x) y) + inner ℝ ((fderiv ℝ f x) y) (g x)

theorem deriv_inner_apply' {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] [InnerProductSpace' ℝ F] {f g : ℝ → F} {x : ℝ} (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) : deriv (fun (t : ℝ) => inner ℝ (f t) (g t)) x = inner ℝ (f x) (deriv g x) + inner ℝ (deriv f x) (g x)

theorem DifferentiableAt.inner' {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [InnerProductSpace' ℝ F] {f g : E → F} {x : E} (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) : DifferentiableAt ℝ (fun (x : E) => Inner.inner ℝ (f x) (g x)) x