Physlib.Mathematics.InnerProductSpace.Calculus

Imports
                /-
Copyright (c) 2025 Tomas Skrivan. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Tomas Skrivan
-/
module

public import Physlib.Mathematics.InnerProductSpace.Basic

              
                Generalization of calculus results to InnerProductSpace'
              

              @[expose] public sectionlocal notation "⟪" x ", " y "⟫" => inner ℝ x ylemma HasFDerivAt.inner' {f g : E → F}
    {f' g' : E →L[ℝ] F} (hf : HasFDerivAt f f' x) (hg : HasFDerivAt g g' x) :
    HasFDerivAt (fun t => ⟪f t, g t⟫) ((fderivInnerCLM' (f x, g x)).comp <| f'.prod g') x := byE:Type u_2F:Type u_3inst✝⁴:NormedAddCommGroup Einst✝³:NormedSpace ℝ Einst✝²:NormedAddCommGroup Finst✝¹:NormedSpace ℝ Finst✝:InnerProductSpace' ℝ Fx:Ef:E → Fg:E → Ff':E →L[ℝ] Fg':E →L[ℝ] Fhf:HasFDerivAt f f' xhg:HasFDerivAt g g' x⊢ HasFDerivAt (fun t => ⟪f t, g t⟫) (fderivInnerCLM' (f x, g x) ∘SL f'.prod g') x
  exact isBoundedBilinearMap_inner' (E := F)
    |>.hasFDerivAt (f x, g x) |>.comp x (hf.prodMk hg)All goals completed! 🐙

-- todo: move this
lemma fderiv_inner_apply'
    {f g : E → F} {x : E}
    (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) (y : E) :
    fderiv ℝ (fun t => ⟪f t, g t⟫) x y = ⟪f x, fderiv ℝ g x y⟫ + ⟪fderiv ℝ f x y, g x⟫ := byE:Type u_2F:Type u_3inst✝⁴:NormedAddCommGroup Einst✝³:NormedSpace ℝ Einst✝²:NormedAddCommGroup Finst✝¹:NormedSpace ℝ Finst✝:InnerProductSpace' ℝ Ff:E → Fg:E → Fx:Ehf:DifferentiableAt ℝ f xhg:DifferentiableAt ℝ g xy:E⊢ (fderiv ℝ (fun t => ⟪f t, g t⟫) x) y = ⟪f x, (fderiv ℝ g x) y⟫ + ⟪(fderiv ℝ f x) y, g x⟫
  rw [(hf.hasFDerivAt.inner' hg.hasFDerivAt).fderivE:Type u_2F:Type u_3inst✝⁴:NormedAddCommGroup Einst✝³:NormedSpace ℝ Einst✝²:NormedAddCommGroup Finst✝¹:NormedSpace ℝ Finst✝:InnerProductSpace' ℝ Ff:E → Fg:E → Fx:Ehf:DifferentiableAt ℝ f xhg:DifferentiableAt ℝ g xy:E⊢ (fderivInnerCLM' (f x, g x) ∘SL (fderiv ℝ f x).prod (fderiv ℝ g x)) y =
  ⟪f x, (fderiv ℝ g x) y⟫ + ⟪(fderiv ℝ f x) y, g x⟫E:Type u_2F:Type u_3inst✝⁴:NormedAddCommGroup Einst✝³:NormedSpace ℝ Einst✝²:NormedAddCommGroup Finst✝¹:NormedSpace ℝ Finst✝:InnerProductSpace' ℝ Ff:E → Fg:E → Fx:Ehf:DifferentiableAt ℝ f xhg:DifferentiableAt ℝ g xy:E⊢ (fderivInnerCLM' (f x, g x) ∘SL (fderiv ℝ f x).prod (fderiv ℝ g x)) y =
  ⟪f x, (fderiv ℝ g x) y⟫ + ⟪(fderiv ℝ f x) y, g x⟫]E:Type u_2F:Type u_3inst✝⁴:NormedAddCommGroup Einst✝³:NormedSpace ℝ Einst✝²:NormedAddCommGroup Finst✝¹:NormedSpace ℝ Finst✝:InnerProductSpace' ℝ Ff:E → Fg:E → Fx:Ehf:DifferentiableAt ℝ f xhg:DifferentiableAt ℝ g xy:E⊢ (fderivInnerCLM' (f x, g x) ∘SL (fderiv ℝ f x).prod (fderiv ℝ g x)) y =
  ⟪f x, (fderiv ℝ g x) y⟫ + ⟪(fderiv ℝ f x) y, g x⟫
  rflAll goals completed! 🐙-- todo: move this
lemma deriv_inner_apply'
    {f g : ℝ → F} {x : ℝ}
    (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) :
    deriv (fun t => ⟪f t, g t⟫) x = ⟪f x, deriv g x⟫ + ⟪deriv f x, g x⟫ :=
  fderiv_inner_apply' hf hg 1-- todo: move this
@[fun_prop]
lemma DifferentiableAt.inner' {f g : E → F} {x}
    (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) :
    DifferentiableAt ℝ (fun x => ⟪f x, g x⟫) x := byE:Type u_2F:Type u_3inst✝⁴:NormedAddCommGroup Einst✝³:NormedSpace ℝ Einst✝²:NormedAddCommGroup Finst✝¹:NormedSpace ℝ Finst✝:InnerProductSpace' ℝ Ff:E → Fg:E → Fx:Ehf:DifferentiableAt ℝ f xhg:DifferentiableAt ℝ g x⊢ DifferentiableAt ℝ (fun x => ⟪f x, g x⟫) x
  apply HasFDerivAt.differentiableAthE:Type u_2F:Type u_3inst✝⁴:NormedAddCommGroup Einst✝³:NormedSpace ℝ Einst✝²:NormedAddCommGroup Finst✝¹:NormedSpace ℝ Finst✝:InnerProductSpace' ℝ Ff:E → Fg:E → Fx:Ehf:DifferentiableAt ℝ f xhg:DifferentiableAt ℝ g x⊢ HasFDerivAt (fun x => ⟪f x, g x⟫) ?f' xf'E:Type u_2F:Type u_3inst✝⁴:NormedAddCommGroup Einst✝³:NormedSpace ℝ Einst✝²:NormedAddCommGroup Finst✝¹:NormedSpace ℝ Finst✝:InnerProductSpace' ℝ Ff:E → Fg:E → Fx:Ehf:DifferentiableAt ℝ f xhg:DifferentiableAt ℝ g x⊢ E →L[ℝ] ℝ
  exact hf.hasFDerivAt.inner' hg.hasFDerivAtAll goals completed! 🐙