Physlib.Mathematics.Calculus.AdjFDeriv

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 Mathlib.Analysis.Calculus.Gradient.Basic
public import Physlib.Mathematics.FDerivCurry
public import Physlib.Mathematics.InnerProductSpace.Adjoint
public import Physlib.Mathematics.InnerProductSpace.Calculus

Adjoint Fréchet derivative

adjFDeriv 𝕜 f x = (fderiv 𝕜 f x).adjoint

The main purpose of defining adjFDeriv is to compute gradient f x = adjFDeriv 𝕜 f x 1. The advantage of working with adjFDeriv is that we can formulate composition theorem.

The reason why we do not want to compute fderiv and then adjoint is that to compute fderiv 𝕜 f or adjoint f we decompose f = f₁ ∘ ... ∘ fₙ and then apply composition theorem. The problem is that this decomposition has to be done differently for fderiv and adjoint. The problem is that when working with fderiv the natural product type is X × Y but when working with adjoint the natural product is WithLp 2 (X × Y). For example:

              @[expose] public section

protected lemma HasAdjFDerivAt.adjFDeriv {f : E → F} {f'} {x} (hf : HasAdjFDerivAt 𝕜 f f' x) :
    adjFDeriv 𝕜 f x = f' := by𝕜:Type u_1inst✝⁶:RCLike 𝕜E:Type u_2inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 Einst✝³:InnerProductSpace' 𝕜 EF:Type u_3inst✝²:NormedAddCommGroup Finst✝¹:NormedSpace 𝕜 Finst✝:InnerProductSpace' 𝕜 Ff:E → Ff':F → Ex:Ehf:HasAdjFDerivAt 𝕜 f f' x⊢ adjFDeriv 𝕜 f x = f'
  unfold adjFDeriv𝕜:Type u_1inst✝⁶:RCLike 𝕜E:Type u_2inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 Einst✝³:InnerProductSpace' 𝕜 EF:Type u_3inst✝²:NormedAddCommGroup Finst✝¹:NormedSpace 𝕜 Finst✝:InnerProductSpace' 𝕜 Ff:E → Ff':F → Ex:Ehf:HasAdjFDerivAt 𝕜 f f' x⊢ (fun dy => adjoint 𝕜 (⇑(fderiv 𝕜 f x)) dy) = f'; funext y𝕜:Type u_1inst✝⁶:RCLike 𝕜E:Type u_2inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 Einst✝³:InnerProductSpace' 𝕜 EF:Type u_3inst✝²:NormedAddCommGroup Finst✝¹:NormedSpace 𝕜 Finst✝:InnerProductSpace' 𝕜 Ff:E → Ff':F → Ex:Ehf:HasAdjFDerivAt 𝕜 f f' xy:F⊢ adjoint 𝕜 (⇑(fderiv 𝕜 f x)) y = f' y;
  rw[hf.hasAdjoint_fderiv.adjoint𝕜:Type u_1inst✝⁶:RCLike 𝕜E:Type u_2inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 Einst✝³:InnerProductSpace' 𝕜 EF:Type u_3inst✝²:NormedAddCommGroup Finst✝¹:NormedSpace 𝕜 Finst✝:InnerProductSpace' 𝕜 Ff:E → Ff':F → Ex:Ehf:HasAdjFDerivAt 𝕜 f f' xy:F⊢ f' y = f' yAll goals completed! 🐙]All goals completed! 🐙lemma adjoint.isBoundedBilinearMap_real :
    IsBoundedBilinearMap ℝ (fun (fy : (X →L[ℝ] Y)×Y) => fy.1.adjoint fy.2) :=
{
  add_left := byX:Type u_6inst✝⁵:NormedAddCommGroup Xinst✝⁴:InnerProductSpace ℝ Xinst✝³:CompleteSpace XY:Type u_7inst✝²:NormedAddCommGroup Yinst✝¹:InnerProductSpace ℝ Yinst✝:CompleteSpace Y⊢ ∀ (x₁ x₂ : X →L[ℝ] Y) (y : Y),
  (adjoint (x₁ + x₂, y).1) (x₁ + x₂, y).2 = (adjoint (x₁, y).1) (x₁, y).2 + (adjoint (x₂, y).1) (x₂, y).2 simpAll goals completed! 🐙
  smul_left := byX:Type u_6inst✝⁵:NormedAddCommGroup Xinst✝⁴:InnerProductSpace ℝ Xinst✝³:CompleteSpace XY:Type u_7inst✝²:NormedAddCommGroup Yinst✝¹:InnerProductSpace ℝ Yinst✝:CompleteSpace Y⊢ ∀ (c : ℝ) (x : X →L[ℝ] Y) (y : Y), (adjoint (c • x, y).1) (c • x, y).2 = c • (adjoint (x, y).1) (x, y).2 simpAll goals completed! 🐙
  add_right := byX:Type u_6inst✝⁵:NormedAddCommGroup Xinst✝⁴:InnerProductSpace ℝ Xinst✝³:CompleteSpace XY:Type u_7inst✝²:NormedAddCommGroup Yinst✝¹:InnerProductSpace ℝ Yinst✝:CompleteSpace Y⊢ ∀ (x : X →L[ℝ] Y) (y₁ y₂ : Y),
  (adjoint (x, y₁ + y₂).1) (x, y₁ + y₂).2 = (adjoint (x, y₁).1) (x, y₁).2 + (adjoint (x, y₂).1) (x, y₂).2 simpAll goals completed! 🐙
  smul_right := byX:Type u_6inst✝⁵:NormedAddCommGroup Xinst✝⁴:InnerProductSpace ℝ Xinst✝³:CompleteSpace XY:Type u_7inst✝²:NormedAddCommGroup Yinst✝¹:InnerProductSpace ℝ Yinst✝:CompleteSpace Y⊢ ∀ (c : ℝ) (x : X →L[ℝ] Y) (y : Y), (adjoint (x, c • y).1) (x, c • y).2 = c • (adjoint (x, y).1) (x, y).2 simpAll goals completed! 🐙
  bound := byX:Type u_6inst✝⁵:NormedAddCommGroup Xinst✝⁴:InnerProductSpace ℝ Xinst✝³:CompleteSpace XY:Type u_7inst✝²:NormedAddCommGroup Yinst✝¹:InnerProductSpace ℝ Yinst✝:CompleteSpace Y⊢ ∃ C > 0, ∀ (x : X →L[ℝ] Y) (y : Y), ‖(adjoint (x, y).1) (x, y).2‖ ≤ C * ‖x‖ * ‖y‖
    simp only [gt_iff_lt]X:Type u_6inst✝⁵:NormedAddCommGroup Xinst✝⁴:InnerProductSpace ℝ Xinst✝³:CompleteSpace XY:Type u_7inst✝²:NormedAddCommGroup Yinst✝¹:InnerProductSpace ℝ Yinst✝:CompleteSpace Y⊢ ∃ C, 0 < C ∧ ∀ (x : X →L[ℝ] Y) (y : Y), ‖(adjoint x) y‖ ≤ C * ‖x‖ * ‖y‖
    use 1hX:Type u_6inst✝⁵:NormedAddCommGroup Xinst✝⁴:InnerProductSpace ℝ Xinst✝³:CompleteSpace XY:Type u_7inst✝²:NormedAddCommGroup Yinst✝¹:InnerProductSpace ℝ Yinst✝:CompleteSpace Y⊢ 0 < 1 ∧ ∀ (x : X →L[ℝ] Y) (y : Y), ‖(adjoint x) y‖ ≤ 1 * ‖x‖ * ‖y‖
    constructorh.leftX:Type u_6inst✝⁵:NormedAddCommGroup Xinst✝⁴:InnerProductSpace ℝ Xinst✝³:CompleteSpace XY:Type u_7inst✝²:NormedAddCommGroup Yinst✝¹:InnerProductSpace ℝ Yinst✝:CompleteSpace Y⊢ 0 < 1h.rightX:Type u_6inst✝⁵:NormedAddCommGroup Xinst✝⁴:InnerProductSpace ℝ Xinst✝³:CompleteSpace XY:Type u_7inst✝²:NormedAddCommGroup Yinst✝¹:InnerProductSpace ℝ Yinst✝:CompleteSpace Y⊢ ∀ (x : X →L[ℝ] Y) (y : Y), ‖(adjoint x) y‖ ≤ 1 * ‖x‖ * ‖y‖
    ·h.leftX:Type u_6inst✝⁵:NormedAddCommGroup Xinst✝⁴:InnerProductSpace ℝ Xinst✝³:CompleteSpace XY:Type u_7inst✝²:NormedAddCommGroup Yinst✝¹:InnerProductSpace ℝ Yinst✝:CompleteSpace Y⊢ 0 < 1 simpAll goals completed! 🐙
    ·h.rightX:Type u_6inst✝⁵:NormedAddCommGroup Xinst✝⁴:InnerProductSpace ℝ Xinst✝³:CompleteSpace XY:Type u_7inst✝²:NormedAddCommGroup Yinst✝¹:InnerProductSpace ℝ Yinst✝:CompleteSpace Y⊢ ∀ (x : X →L[ℝ] Y) (y : Y), ‖(adjoint x) y‖ ≤ 1 * ‖x‖ * ‖y‖ intro f yh.rightX:Type u_6inst✝⁵:NormedAddCommGroup Xinst✝⁴:InnerProductSpace ℝ Xinst✝³:CompleteSpace XY:Type u_7inst✝²:NormedAddCommGroup Yinst✝¹:InnerProductSpace ℝ Yinst✝:CompleteSpace Yf:X →L[ℝ] Yy:Y⊢ ‖(adjoint f) y‖ ≤ 1 * ‖f‖ * ‖y‖
      trans ‖f.adjoint‖ * ‖y‖X:Type u_6inst✝⁵:NormedAddCommGroup Xinst✝⁴:InnerProductSpace ℝ Xinst✝³:CompleteSpace XY:Type u_7inst✝²:NormedAddCommGroup Yinst✝¹:InnerProductSpace ℝ Yinst✝:CompleteSpace Yf:X →L[ℝ] Yy:Y⊢ ‖(adjoint f) y‖ ≤ ‖adjoint f‖ * ‖y‖X:Type u_6inst✝⁵:NormedAddCommGroup Xinst✝⁴:InnerProductSpace ℝ Xinst✝³:CompleteSpace XY:Type u_7inst✝²:NormedAddCommGroup Yinst✝¹:InnerProductSpace ℝ Yinst✝:CompleteSpace Yf:X →L[ℝ] Yy:Y⊢ ‖adjoint f‖ * ‖y‖ ≤ 1 * ‖f‖ * ‖y‖
      apply ContinuousLinearMap.le_opNormX:Type u_6inst✝⁵:NormedAddCommGroup Xinst✝⁴:InnerProductSpace ℝ Xinst✝³:CompleteSpace XY:Type u_7inst✝²:NormedAddCommGroup Yinst✝¹:InnerProductSpace ℝ Yinst✝:CompleteSpace Yf:X →L[ℝ] Yy:Y⊢ ‖adjoint f‖ * ‖y‖ ≤ 1 * ‖f‖ * ‖y‖
      simpAll goals completed! 🐙
}lemma gradient_eq_adjFDeriv
    {f : U → 𝕜} {x : U} (hf : DifferentiableAt 𝕜 f x) :
    gradient f x = adjFDeriv 𝕜 f x 1 := by𝕜:Type u_1inst✝³:RCLike 𝕜U:Type u_5inst✝²:NormedAddCommGroup Uinst✝¹:InnerProductSpace 𝕜 Uinst✝:CompleteSpace Uf:U → 𝕜x:Uhf:DifferentiableAt 𝕜 f x⊢ gradient f x = adjFDeriv 𝕜 f x 1
  apply ext_inner_right 𝕜𝕜:Type u_1inst✝³:RCLike 𝕜U:Type u_5inst✝²:NormedAddCommGroup Uinst✝¹:InnerProductSpace 𝕜 Uinst✝:CompleteSpace Uf:U → 𝕜x:Uhf:DifferentiableAt 𝕜 f x⊢ ∀ (v : U), inner 𝕜 (gradient f x) v = inner 𝕜 (adjFDeriv 𝕜 f x 1) v
  unfold gradient𝕜:Type u_1inst✝³:RCLike 𝕜U:Type u_5inst✝²:NormedAddCommGroup Uinst✝¹:InnerProductSpace 𝕜 Uinst✝:CompleteSpace Uf:U → 𝕜x:Uhf:DifferentiableAt 𝕜 f x⊢ ∀ (v : U), inner 𝕜 ((InnerProductSpace.toDual 𝕜 U).symm (fderiv 𝕜 f x)) v = inner 𝕜 (adjFDeriv 𝕜 f x 1) v
  simp [hf.hasAdjFDerivAt.hasAdjoint_fderiv.adjoint_inner_left]All goals completed! 🐙attribute [fun_prop] HasAdjFDerivAt.differentiableAtlemma hasAdjFDerivAt_id (x : E) : HasAdjFDerivAt 𝕜 (fun x : E => x) (fun dx => dx) x where
  differentiableAt := by𝕜:Type u_1inst✝³:RCLike 𝕜E:Type u_2inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace 𝕜 Einst✝:InnerProductSpace' 𝕜 Ex:E⊢ DifferentiableAt 𝕜 (fun x => x) x fun_propAll goals completed! 🐙
  hasAdjoint_fderiv := by𝕜:Type u_1inst✝³:RCLike 𝕜E:Type u_2inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace 𝕜 Einst✝:InnerProductSpace' 𝕜 Ex:E⊢ HasAdjoint 𝕜 ⇑(fderiv 𝕜 (fun x => x) x) fun dx => dx
    simp𝕜:Type u_1inst✝³:RCLike 𝕜E:Type u_2inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace 𝕜 Einst✝:InnerProductSpace' 𝕜 Ex:E⊢ HasAdjoint 𝕜 id fun x => x; apply hasAdjoint_idAll goals completed! 🐙

lemma adjFDeriv_id : adjFDeriv 𝕜 (fun x : E => x) = fun _ dx => dx := by𝕜:Type u_1inst✝³:RCLike 𝕜E:Type u_2inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace 𝕜 Einst✝:InnerProductSpace' 𝕜 E⊢ (adjFDeriv 𝕜 fun x => x) = fun x dx => dx
  funext x𝕜:Type u_1inst✝³:RCLike 𝕜E:Type u_2inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace 𝕜 Einst✝:InnerProductSpace' 𝕜 Ex:E⊢ adjFDeriv 𝕜 (fun x => x) x = fun dx => dx
  rw[HasAdjFDerivAt.adjFDeriv (hasAdjFDerivAt_id x)𝕜:Type u_1inst✝³:RCLike 𝕜E:Type u_2inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace 𝕜 Einst✝:InnerProductSpace' 𝕜 Ex:E⊢ (fun dx => dx) = fun dx => dxAll goals completed! 🐙]All goals completed! 🐙lemma adjFDeriv_id' : adjFDeriv 𝕜 (id : E → E) = fun _ dx => dx := by𝕜:Type u_1inst✝³:RCLike 𝕜E:Type u_2inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace 𝕜 Einst✝:InnerProductSpace' 𝕜 E⊢ adjFDeriv 𝕜 id = fun x dx => dx
  exact adjFDeriv_idAll goals completed! 🐙lemma hasAdjFDerivAt_const (x : E) (y : F) :
    HasAdjFDerivAt 𝕜 (fun _ : E => y) (fun _ => 0) x where
  differentiableAt := by𝕜:Type u_1inst✝⁶:RCLike 𝕜E:Type u_2inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 Einst✝³:InnerProductSpace' 𝕜 EF:Type u_3inst✝²:NormedAddCommGroup Finst✝¹:NormedSpace 𝕜 Finst✝:InnerProductSpace' 𝕜 Fx:Ey:F⊢ DifferentiableAt 𝕜 (fun x => y) x fun_propAll goals completed! 🐙
  hasAdjoint_fderiv := by𝕜:Type u_1inst✝⁶:RCLike 𝕜E:Type u_2inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 Einst✝³:InnerProductSpace' 𝕜 EF:Type u_3inst✝²:NormedAddCommGroup Finst✝¹:NormedSpace 𝕜 Finst✝:InnerProductSpace' 𝕜 Fx:Ey:F⊢ HasAdjoint 𝕜 ⇑(fderiv 𝕜 (fun x => y) x) fun x => 0
    simp𝕜:Type u_1inst✝⁶:RCLike 𝕜E:Type u_2inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 Einst✝³:InnerProductSpace' 𝕜 EF:Type u_3inst✝²:NormedAddCommGroup Finst✝¹:NormedSpace 𝕜 Finst✝:InnerProductSpace' 𝕜 Fx:Ey:F⊢ HasAdjoint 𝕜 ⇑0 fun x => 0; apply hasAdjoint_zeroAll goals completed! 🐙

lemma adjFDeriv_const (y : F) : adjFDeriv 𝕜 (fun _ : E => y) = fun _ _ => 0 := by𝕜:Type u_1inst✝⁶:RCLike 𝕜E:Type u_2inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 Einst✝³:InnerProductSpace' 𝕜 EF:Type u_3inst✝²:NormedAddCommGroup Finst✝¹:NormedSpace 𝕜 Finst✝:InnerProductSpace' 𝕜 Fy:F⊢ (adjFDeriv 𝕜 fun x => y) = fun x x_1 => 0
  funext x𝕜:Type u_1inst✝⁶:RCLike 𝕜E:Type u_2inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 Einst✝³:InnerProductSpace' 𝕜 EF:Type u_3inst✝²:NormedAddCommGroup Finst✝¹:NormedSpace 𝕜 Finst✝:InnerProductSpace' 𝕜 Fy:Fx:E⊢ adjFDeriv 𝕜 (fun x => y) x = fun x => 0
  rw[HasAdjFDerivAt.adjFDeriv (hasAdjFDerivAt_const x y)𝕜:Type u_1inst✝⁶:RCLike 𝕜E:Type u_2inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 Einst✝³:InnerProductSpace' 𝕜 EF:Type u_3inst✝²:NormedAddCommGroup Finst✝¹:NormedSpace 𝕜 Finst✝:InnerProductSpace' 𝕜 Fy:Fx:E⊢ (fun x => 0) = fun x => 0All goals completed! 🐙]All goals completed! 🐙lemma HasAdjFDerivAt.comp {f : F → G} {g : E → F} {f' g'} {x : E}
    (hf : HasAdjFDerivAt 𝕜 f f' (g x)) (hg : HasAdjFDerivAt 𝕜 g g' x) :
    HasAdjFDerivAt 𝕜 (fun x => f (g x)) (fun dz => g' (f' dz)) x where
  differentiableAt := by𝕜:Type u_1inst✝⁹:RCLike 𝕜E:Type u_2inst✝⁸:NormedAddCommGroup Einst✝⁷:NormedSpace 𝕜 Einst✝⁶:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁵:NormedAddCommGroup Finst✝⁴:NormedSpace 𝕜 Finst✝³:InnerProductSpace' 𝕜 FG:Type u_4inst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace 𝕜 Ginst✝:InnerProductSpace' 𝕜 Gf:F → Gg:E → Ff':G → Fg':F → Ex:Ehf:HasAdjFDerivAt 𝕜 f f' (g x)hg:HasAdjFDerivAt 𝕜 g g' x⊢ DifferentiableAt 𝕜 (fun x => f (g x)) x
    fun_propAll goals completed! 🐙
  hasAdjoint_fderiv := by𝕜:Type u_1inst✝⁹:RCLike 𝕜E:Type u_2inst✝⁸:NormedAddCommGroup Einst✝⁷:NormedSpace 𝕜 Einst✝⁶:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁵:NormedAddCommGroup Finst✝⁴:NormedSpace 𝕜 Finst✝³:InnerProductSpace' 𝕜 FG:Type u_4inst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace 𝕜 Ginst✝:InnerProductSpace' 𝕜 Gf:F → Gg:E → Ff':G → Fg':F → Ex:Ehf:HasAdjFDerivAt 𝕜 f f' (g x)hg:HasAdjFDerivAt 𝕜 g g' x⊢ HasAdjoint 𝕜 ⇑(fderiv 𝕜 (fun x => f (g x)) x) fun dz => g' (f' dz)
    simp (disch:=fun_prop) [fderiv_fun_comp]𝕜:Type u_1inst✝⁹:RCLike 𝕜E:Type u_2inst✝⁸:NormedAddCommGroup Einst✝⁷:NormedSpace 𝕜 Einst✝⁶:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁵:NormedAddCommGroup Finst✝⁴:NormedSpace 𝕜 Finst✝³:InnerProductSpace' 𝕜 FG:Type u_4inst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace 𝕜 Ginst✝:InnerProductSpace' 𝕜 Gf:F → Gg:E → Ff':G → Fg':F → Ex:Ehf:HasAdjFDerivAt 𝕜 f f' (g x)hg:HasAdjFDerivAt 𝕜 g g' x⊢ HasAdjoint 𝕜 ⇑(fderiv 𝕜 f (g x) ∘SL fderiv 𝕜 g x) fun dz => g' (f' dz)
    exact hf.hasAdjoint_fderiv.comp hg.hasAdjoint_fderivAll goals completed! 🐙lemma adjFDeriv_comp [CompleteSpace E] [CompleteSpace F] [CompleteSpace G]
    {f : F → G} {g : E → F} {x : E}
    (hf : DifferentiableAt 𝕜 f (g x)) (hg : DifferentiableAt 𝕜 g x) :
    adjFDeriv 𝕜 (fun x => f (g x)) x = fun dy => adjFDeriv 𝕜 g x (adjFDeriv 𝕜 f (g x) dy) := by𝕜:Type u_1inst✝¹²:RCLike 𝕜E:Type u_2inst✝¹¹:NormedAddCommGroup Einst✝¹⁰:NormedSpace 𝕜 Einst✝⁹:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁸:NormedAddCommGroup Finst✝⁷:NormedSpace 𝕜 Finst✝⁶:InnerProductSpace' 𝕜 FG:Type u_4inst✝⁵:NormedAddCommGroup Ginst✝⁴:NormedSpace 𝕜 Ginst✝³:InnerProductSpace' 𝕜 Ginst✝²:CompleteSpace Einst✝¹:CompleteSpace Finst✝:CompleteSpace Gf:F → Gg:E → Fx:Ehf:DifferentiableAt 𝕜 f (g x)hg:DifferentiableAt 𝕜 g x⊢ adjFDeriv 𝕜 (fun x => f (g x)) x = fun dy => adjFDeriv 𝕜 g x (adjFDeriv 𝕜 f (g x) dy)
  apply HasAdjFDerivAt.adjFDeriv𝕜:Type u_1inst✝¹²:RCLike 𝕜E:Type u_2inst✝¹¹:NormedAddCommGroup Einst✝¹⁰:NormedSpace 𝕜 Einst✝⁹:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁸:NormedAddCommGroup Finst✝⁷:NormedSpace 𝕜 Finst✝⁶:InnerProductSpace' 𝕜 FG:Type u_4inst✝⁵:NormedAddCommGroup Ginst✝⁴:NormedSpace 𝕜 Ginst✝³:InnerProductSpace' 𝕜 Ginst✝²:CompleteSpace Einst✝¹:CompleteSpace Finst✝:CompleteSpace Gf:F → Gg:E → Fx:Ehf:DifferentiableAt 𝕜 f (g x)hg:DifferentiableAt 𝕜 g x⊢ HasAdjFDerivAt 𝕜 (fun x => f (g x)) (fun dy => adjFDeriv 𝕜 g x (adjFDeriv 𝕜 f (g x) dy)) x
  apply HasAdjFDerivAt.comphf𝕜:Type u_1inst✝¹²:RCLike 𝕜E:Type u_2inst✝¹¹:NormedAddCommGroup Einst✝¹⁰:NormedSpace 𝕜 Einst✝⁹:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁸:NormedAddCommGroup Finst✝⁷:NormedSpace 𝕜 Finst✝⁶:InnerProductSpace' 𝕜 FG:Type u_4inst✝⁵:NormedAddCommGroup Ginst✝⁴:NormedSpace 𝕜 Ginst✝³:InnerProductSpace' 𝕜 Ginst✝²:CompleteSpace Einst✝¹:CompleteSpace Finst✝:CompleteSpace Gf:F → Gg:E → Fx:Ehf:DifferentiableAt 𝕜 f (g x)hg:DifferentiableAt 𝕜 g x⊢ HasAdjFDerivAt 𝕜 f (adjFDeriv 𝕜 f (g x)) (g x)hg𝕜:Type u_1inst✝¹²:RCLike 𝕜E:Type u_2inst✝¹¹:NormedAddCommGroup Einst✝¹⁰:NormedSpace 𝕜 Einst✝⁹:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁸:NormedAddCommGroup Finst✝⁷:NormedSpace 𝕜 Finst✝⁶:InnerProductSpace' 𝕜 FG:Type u_4inst✝⁵:NormedAddCommGroup Ginst✝⁴:NormedSpace 𝕜 Ginst✝³:InnerProductSpace' 𝕜 Ginst✝²:CompleteSpace Einst✝¹:CompleteSpace Finst✝:CompleteSpace Gf:F → Gg:E → Fx:Ehf:DifferentiableAt 𝕜 f (g x)hg:DifferentiableAt 𝕜 g x⊢ HasAdjFDerivAt 𝕜 g (adjFDeriv 𝕜 g x) x
  apply hf.hasAdjFDerivAthg𝕜:Type u_1inst✝¹²:RCLike 𝕜E:Type u_2inst✝¹¹:NormedAddCommGroup Einst✝¹⁰:NormedSpace 𝕜 Einst✝⁹:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁸:NormedAddCommGroup Finst✝⁷:NormedSpace 𝕜 Finst✝⁶:InnerProductSpace' 𝕜 FG:Type u_4inst✝⁵:NormedAddCommGroup Ginst✝⁴:NormedSpace 𝕜 Ginst✝³:InnerProductSpace' 𝕜 Ginst✝²:CompleteSpace Einst✝¹:CompleteSpace Finst✝:CompleteSpace Gf:F → Gg:E → Fx:Ehf:DifferentiableAt 𝕜 f (g x)hg:DifferentiableAt 𝕜 g x⊢ HasAdjFDerivAt 𝕜 g (adjFDeriv 𝕜 g x) x
  apply hg.hasAdjFDerivAtAll goals completed! 🐙lemma HasAdjFDerivAt.prodMk {f : E → F} {g : E → G} {f' g'} {x : E}
    (hf : HasAdjFDerivAt 𝕜 f f' x) (hg : HasAdjFDerivAt 𝕜 g g' x) :
    HasAdjFDerivAt 𝕜 (fun x => (f x, g x)) (fun dyz => f' dyz.fst + g' dyz.snd) x where
  differentiableAt := by𝕜:Type u_1inst✝⁹:RCLike 𝕜E:Type u_2inst✝⁸:NormedAddCommGroup Einst✝⁷:NormedSpace 𝕜 Einst✝⁶:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁵:NormedAddCommGroup Finst✝⁴:NormedSpace 𝕜 Finst✝³:InnerProductSpace' 𝕜 FG:Type u_4inst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace 𝕜 Ginst✝:InnerProductSpace' 𝕜 Gf:E → Fg:E → Gf':F → Eg':G → Ex:Ehf:HasAdjFDerivAt 𝕜 f f' xhg:HasAdjFDerivAt 𝕜 g g' x⊢ DifferentiableAt 𝕜 (fun x => (f x, g x)) x fun_propAll goals completed! 🐙
  hasAdjoint_fderiv := by𝕜:Type u_1inst✝⁹:RCLike 𝕜E:Type u_2inst✝⁸:NormedAddCommGroup Einst✝⁷:NormedSpace 𝕜 Einst✝⁶:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁵:NormedAddCommGroup Finst✝⁴:NormedSpace 𝕜 Finst✝³:InnerProductSpace' 𝕜 FG:Type u_4inst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace 𝕜 Ginst✝:InnerProductSpace' 𝕜 Gf:E → Fg:E → Gf':F → Eg':G → Ex:Ehf:HasAdjFDerivAt 𝕜 f f' xhg:HasAdjFDerivAt 𝕜 g g' x⊢ HasAdjoint 𝕜 ⇑(fderiv 𝕜 (fun x => (f x, g x)) x) fun dyz => f' dyz.1 + g' dyz.2
    simp (disch:=fun_prop) [DifferentiableAt.fderiv_prodMk]𝕜:Type u_1inst✝⁹:RCLike 𝕜E:Type u_2inst✝⁸:NormedAddCommGroup Einst✝⁷:NormedSpace 𝕜 Einst✝⁶:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁵:NormedAddCommGroup Finst✝⁴:NormedSpace 𝕜 Finst✝³:InnerProductSpace' 𝕜 FG:Type u_4inst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace 𝕜 Ginst✝:InnerProductSpace' 𝕜 Gf:E → Fg:E → Gf':F → Eg':G → Ex:Ehf:HasAdjFDerivAt 𝕜 f f' xhg:HasAdjFDerivAt 𝕜 g g' x⊢ HasAdjoint 𝕜 ⇑((fderiv 𝕜 f x).prod (fderiv 𝕜 g x)) fun dyz => f' dyz.1 + g' dyz.2
    apply HasAdjoint.prodMkhf𝕜:Type u_1inst✝⁹:RCLike 𝕜E:Type u_2inst✝⁸:NormedAddCommGroup Einst✝⁷:NormedSpace 𝕜 Einst✝⁶:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁵:NormedAddCommGroup Finst✝⁴:NormedSpace 𝕜 Finst✝³:InnerProductSpace' 𝕜 FG:Type u_4inst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace 𝕜 Ginst✝:InnerProductSpace' 𝕜 Gf:E → Fg:E → Gf':F → Eg':G → Ex:Ehf:HasAdjFDerivAt 𝕜 f f' xhg:HasAdjFDerivAt 𝕜 g g' x⊢ HasAdjoint 𝕜 (⇑↑(fderiv 𝕜 f x)) f'hg𝕜:Type u_1inst✝⁹:RCLike 𝕜E:Type u_2inst✝⁸:NormedAddCommGroup Einst✝⁷:NormedSpace 𝕜 Einst✝⁶:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁵:NormedAddCommGroup Finst✝⁴:NormedSpace 𝕜 Finst✝³:InnerProductSpace' 𝕜 FG:Type u_4inst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace 𝕜 Ginst✝:InnerProductSpace' 𝕜 Gf:E → Fg:E → Gf':F → Eg':G → Ex:Ehf:HasAdjFDerivAt 𝕜 f f' xhg:HasAdjFDerivAt 𝕜 g g' x⊢ HasAdjoint 𝕜 (⇑↑(fderiv 𝕜 g x)) g'
    ·hf𝕜:Type u_1inst✝⁹:RCLike 𝕜E:Type u_2inst✝⁸:NormedAddCommGroup Einst✝⁷:NormedSpace 𝕜 Einst✝⁶:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁵:NormedAddCommGroup Finst✝⁴:NormedSpace 𝕜 Finst✝³:InnerProductSpace' 𝕜 FG:Type u_4inst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace 𝕜 Ginst✝:InnerProductSpace' 𝕜 Gf:E → Fg:E → Gf':F → Eg':G → Ex:Ehf:HasAdjFDerivAt 𝕜 f f' xhg:HasAdjFDerivAt 𝕜 g g' x⊢ HasAdjoint 𝕜 (⇑↑(fderiv 𝕜 f x)) f' exact hf.hasAdjoint_fderivAll goals completed! 🐙
    ·hg𝕜:Type u_1inst✝⁹:RCLike 𝕜E:Type u_2inst✝⁸:NormedAddCommGroup Einst✝⁷:NormedSpace 𝕜 Einst✝⁶:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁵:NormedAddCommGroup Finst✝⁴:NormedSpace 𝕜 Finst✝³:InnerProductSpace' 𝕜 FG:Type u_4inst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace 𝕜 Ginst✝:InnerProductSpace' 𝕜 Gf:E → Fg:E → Gf':F → Eg':G → Ex:Ehf:HasAdjFDerivAt 𝕜 f f' xhg:HasAdjFDerivAt 𝕜 g g' x⊢ HasAdjoint 𝕜 (⇑↑(fderiv 𝕜 g x)) g' exact hg.hasAdjoint_fderivAll goals completed! 🐙lemma HasAjdFDerivAt.fst {f : E → F×G} {f'} {x : E} (hf : HasAdjFDerivAt 𝕜 f f' x) :
    HasAdjFDerivAt 𝕜 (fun x => (f x).fst) (fun dy => f' (dy, 0)) x where
  differentiableAt := by𝕜:Type u_1inst✝⁹:RCLike 𝕜E:Type u_2inst✝⁸:NormedAddCommGroup Einst✝⁷:NormedSpace 𝕜 Einst✝⁶:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁵:NormedAddCommGroup Finst✝⁴:NormedSpace 𝕜 Finst✝³:InnerProductSpace' 𝕜 FG:Type u_4inst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace 𝕜 Ginst✝:InnerProductSpace' 𝕜 Gf:E → F × Gf':F × G → Ex:Ehf:HasAdjFDerivAt 𝕜 f f' x⊢ DifferentiableAt 𝕜 (fun x => (f x).1) x fun_propAll goals completed! 🐙
  hasAdjoint_fderiv := by𝕜:Type u_1inst✝⁹:RCLike 𝕜E:Type u_2inst✝⁸:NormedAddCommGroup Einst✝⁷:NormedSpace 𝕜 Einst✝⁶:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁵:NormedAddCommGroup Finst✝⁴:NormedSpace 𝕜 Finst✝³:InnerProductSpace' 𝕜 FG:Type u_4inst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace 𝕜 Ginst✝:InnerProductSpace' 𝕜 Gf:E → F × Gf':F × G → Ex:Ehf:HasAdjFDerivAt 𝕜 f f' x⊢ HasAdjoint 𝕜 ⇑(fderiv 𝕜 (fun x => (f x).1) x) fun dy => f' (dy, 0)
    simp (disch:=fun_prop) [fderiv.fst]𝕜:Type u_1inst✝⁹:RCLike 𝕜E:Type u_2inst✝⁸:NormedAddCommGroup Einst✝⁷:NormedSpace 𝕜 Einst✝⁶:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁵:NormedAddCommGroup Finst✝⁴:NormedSpace 𝕜 Finst✝³:InnerProductSpace' 𝕜 FG:Type u_4inst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace 𝕜 Ginst✝:InnerProductSpace' 𝕜 Gf:E → F × Gf':F × G → Ex:Ehf:HasAdjFDerivAt 𝕜 f f' x⊢ HasAdjoint 𝕜 ⇑(ContinuousLinearMap.fst 𝕜 F G ∘SL fderiv 𝕜 f x) fun dy => f' (dy, 0)
    apply HasAdjoint.fst hf.hasAdjoint_fderivAll goals completed! 🐙lemma adjFDeriv_fst [CompleteSpace E] [CompleteSpace F] [CompleteSpace G]
    {f : E → F×G} {x : E} (hf : DifferentiableAt 𝕜 f x) :
    adjFDeriv 𝕜 (fun x => (f x).fst) x = fun dy => adjFDeriv 𝕜 f x (dy, 0) := by𝕜:Type u_1inst✝¹²:RCLike 𝕜E:Type u_2inst✝¹¹:NormedAddCommGroup Einst✝¹⁰:NormedSpace 𝕜 Einst✝⁹:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁸:NormedAddCommGroup Finst✝⁷:NormedSpace 𝕜 Finst✝⁶:InnerProductSpace' 𝕜 FG:Type u_4inst✝⁵:NormedAddCommGroup Ginst✝⁴:NormedSpace 𝕜 Ginst✝³:InnerProductSpace' 𝕜 Ginst✝²:CompleteSpace Einst✝¹:CompleteSpace Finst✝:CompleteSpace Gf:E → F × Gx:Ehf:DifferentiableAt 𝕜 f x⊢ adjFDeriv 𝕜 (fun x => (f x).1) x = fun dy => adjFDeriv 𝕜 f x (dy, 0)
  apply HasAdjFDerivAt.adjFDeriv𝕜:Type u_1inst✝¹²:RCLike 𝕜E:Type u_2inst✝¹¹:NormedAddCommGroup Einst✝¹⁰:NormedSpace 𝕜 Einst✝⁹:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁸:NormedAddCommGroup Finst✝⁷:NormedSpace 𝕜 Finst✝⁶:InnerProductSpace' 𝕜 FG:Type u_4inst✝⁵:NormedAddCommGroup Ginst✝⁴:NormedSpace 𝕜 Ginst✝³:InnerProductSpace' 𝕜 Ginst✝²:CompleteSpace Einst✝¹:CompleteSpace Finst✝:CompleteSpace Gf:E → F × Gx:Ehf:DifferentiableAt 𝕜 f x⊢ HasAdjFDerivAt 𝕜 (fun x => (f x).1) (fun dy => adjFDeriv 𝕜 f x (dy, 0)) x
  apply HasAjdFDerivAt.fst hf.hasAdjFDerivAtAll goals completed! 🐙

@[simp]
lemma adjFDeriv_prod_fst [CompleteSpace E] [CompleteSpace F] {x : F × E} :
    adjFDeriv 𝕜 (Prod.fst : F × E → F) x = fun a => (a, 0) := by𝕜:Type u_1inst✝⁸:RCLike 𝕜E:Type u_2inst✝⁷:NormedAddCommGroup Einst✝⁶:NormedSpace 𝕜 Einst✝⁵:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁴:NormedAddCommGroup Finst✝³:NormedSpace 𝕜 Finst✝²:InnerProductSpace' 𝕜 Finst✝¹:CompleteSpace Einst✝:CompleteSpace Fx:F × E⊢ adjFDeriv 𝕜 Prod.fst x = fun a => (a, 0)
  change adjFDeriv 𝕜 (fun x => (id x).fst) x = _𝕜:Type u_1inst✝⁸:RCLike 𝕜E:Type u_2inst✝⁷:NormedAddCommGroup Einst✝⁶:NormedSpace 𝕜 Einst✝⁵:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁴:NormedAddCommGroup Finst✝³:NormedSpace 𝕜 Finst✝²:InnerProductSpace' 𝕜 Finst✝¹:CompleteSpace Einst✝:CompleteSpace Fx:F × E⊢ adjFDeriv 𝕜 (fun x => (id x).1) x = fun a => (a, 0)
  rw [adjFDeriv_fst𝕜:Type u_1inst✝⁸:RCLike 𝕜E:Type u_2inst✝⁷:NormedAddCommGroup Einst✝⁶:NormedSpace 𝕜 Einst✝⁵:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁴:NormedAddCommGroup Finst✝³:NormedSpace 𝕜 Finst✝²:InnerProductSpace' 𝕜 Finst✝¹:CompleteSpace Einst✝:CompleteSpace Fx:F × E⊢ (fun dy => adjFDeriv 𝕜 id x (dy, 0)) = fun a => (a, 0)𝕜:Type u_1inst✝⁸:RCLike 𝕜E:Type u_2inst✝⁷:NormedAddCommGroup Einst✝⁶:NormedSpace 𝕜 Einst✝⁵:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁴:NormedAddCommGroup Finst✝³:NormedSpace 𝕜 Finst✝²:InnerProductSpace' 𝕜 Finst✝¹:CompleteSpace Einst✝:CompleteSpace Fx:F × E⊢ DifferentiableAt 𝕜 id x𝕜:Type u_1inst✝⁸:RCLike 𝕜E:Type u_2inst✝⁷:NormedAddCommGroup Einst✝⁶:NormedSpace 𝕜 Einst✝⁵:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁴:NormedAddCommGroup Finst✝³:NormedSpace 𝕜 Finst✝²:InnerProductSpace' 𝕜 Finst✝¹:CompleteSpace Einst✝:CompleteSpace Fx:F × E⊢ (fun dy => adjFDeriv 𝕜 id x (dy, 0)) = fun a => (a, 0)𝕜:Type u_1inst✝⁸:RCLike 𝕜E:Type u_2inst✝⁷:NormedAddCommGroup Einst✝⁶:NormedSpace 𝕜 Einst✝⁵:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁴:NormedAddCommGroup Finst✝³:NormedSpace 𝕜 Finst✝²:InnerProductSpace' 𝕜 Finst✝¹:CompleteSpace Einst✝:CompleteSpace Fx:F × E⊢ DifferentiableAt 𝕜 id x]𝕜:Type u_1inst✝⁸:RCLike 𝕜E:Type u_2inst✝⁷:NormedAddCommGroup Einst✝⁶:NormedSpace 𝕜 Einst✝⁵:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁴:NormedAddCommGroup Finst✝³:NormedSpace 𝕜 Finst✝²:InnerProductSpace' 𝕜 Finst✝¹:CompleteSpace Einst✝:CompleteSpace Fx:F × E⊢ (fun dy => adjFDeriv 𝕜 id x (dy, 0)) = fun a => (a, 0)𝕜:Type u_1inst✝⁸:RCLike 𝕜E:Type u_2inst✝⁷:NormedAddCommGroup Einst✝⁶:NormedSpace 𝕜 Einst✝⁵:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁴:NormedAddCommGroup Finst✝³:NormedSpace 𝕜 Finst✝²:InnerProductSpace' 𝕜 Finst✝¹:CompleteSpace Einst✝:CompleteSpace Fx:F × E⊢ DifferentiableAt 𝕜 id x
  funext dy𝕜:Type u_1inst✝⁸:RCLike 𝕜E:Type u_2inst✝⁷:NormedAddCommGroup Einst✝⁶:NormedSpace 𝕜 Einst✝⁵:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁴:NormedAddCommGroup Finst✝³:NormedSpace 𝕜 Finst✝²:InnerProductSpace' 𝕜 Finst✝¹:CompleteSpace Einst✝:CompleteSpace Fx:F × Edy:F⊢ adjFDeriv 𝕜 id x (dy, 0) = (dy, 0)𝕜:Type u_1inst✝⁸:RCLike 𝕜E:Type u_2inst✝⁷:NormedAddCommGroup Einst✝⁶:NormedSpace 𝕜 Einst✝⁵:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁴:NormedAddCommGroup Finst✝³:NormedSpace 𝕜 Finst✝²:InnerProductSpace' 𝕜 Finst✝¹:CompleteSpace Einst✝:CompleteSpace Fx:F × E⊢ DifferentiableAt 𝕜 id x
  rw [adjFDeriv_id'𝕜:Type u_1inst✝⁸:RCLike 𝕜E:Type u_2inst✝⁷:NormedAddCommGroup Einst✝⁶:NormedSpace 𝕜 Einst✝⁵:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁴:NormedAddCommGroup Finst✝³:NormedSpace 𝕜 Finst✝²:InnerProductSpace' 𝕜 Finst✝¹:CompleteSpace Einst✝:CompleteSpace Fx:F × Edy:F⊢ (fun x dx => dx) x (dy, 0) = (dy, 0)𝕜:Type u_1inst✝⁸:RCLike 𝕜E:Type u_2inst✝⁷:NormedAddCommGroup Einst✝⁶:NormedSpace 𝕜 Einst✝⁵:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁴:NormedAddCommGroup Finst✝³:NormedSpace 𝕜 Finst✝²:InnerProductSpace' 𝕜 Finst✝¹:CompleteSpace Einst✝:CompleteSpace Fx:F × E⊢ DifferentiableAt 𝕜 id x𝕜:Type u_1inst✝⁸:RCLike 𝕜E:Type u_2inst✝⁷:NormedAddCommGroup Einst✝⁶:NormedSpace 𝕜 Einst✝⁵:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁴:NormedAddCommGroup Finst✝³:NormedSpace 𝕜 Finst✝²:InnerProductSpace' 𝕜 Finst✝¹:CompleteSpace Einst✝:CompleteSpace Fx:F × E⊢ DifferentiableAt 𝕜 id x]𝕜:Type u_1inst✝⁸:RCLike 𝕜E:Type u_2inst✝⁷:NormedAddCommGroup Einst✝⁶:NormedSpace 𝕜 Einst✝⁵:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁴:NormedAddCommGroup Finst✝³:NormedSpace 𝕜 Finst✝²:InnerProductSpace' 𝕜 Finst✝¹:CompleteSpace Einst✝:CompleteSpace Fx:F × E⊢ DifferentiableAt 𝕜 id x
  simpAll goals completed! 🐙lemma HasAjdFDerivAt.snd {f : E → F×G} {f'} {x : E} (hf : HasAdjFDerivAt 𝕜 f f' x) :
    HasAdjFDerivAt 𝕜 (fun x => (f x).snd) (fun dz => f' (0, dz)) x where
  differentiableAt := by𝕜:Type u_1inst✝⁹:RCLike 𝕜E:Type u_2inst✝⁸:NormedAddCommGroup Einst✝⁷:NormedSpace 𝕜 Einst✝⁶:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁵:NormedAddCommGroup Finst✝⁴:NormedSpace 𝕜 Finst✝³:InnerProductSpace' 𝕜 FG:Type u_4inst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace 𝕜 Ginst✝:InnerProductSpace' 𝕜 Gf:E → F × Gf':F × G → Ex:Ehf:HasAdjFDerivAt 𝕜 f f' x⊢ DifferentiableAt 𝕜 (fun x => (f x).2) x fun_propAll goals completed! 🐙
  hasAdjoint_fderiv := by𝕜:Type u_1inst✝⁹:RCLike 𝕜E:Type u_2inst✝⁸:NormedAddCommGroup Einst✝⁷:NormedSpace 𝕜 Einst✝⁶:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁵:NormedAddCommGroup Finst✝⁴:NormedSpace 𝕜 Finst✝³:InnerProductSpace' 𝕜 FG:Type u_4inst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace 𝕜 Ginst✝:InnerProductSpace' 𝕜 Gf:E → F × Gf':F × G → Ex:Ehf:HasAdjFDerivAt 𝕜 f f' x⊢ HasAdjoint 𝕜 ⇑(fderiv 𝕜 (fun x => (f x).2) x) fun dz => f' (0, dz)
    simp (disch:=fun_prop) [fderiv.snd]𝕜:Type u_1inst✝⁹:RCLike 𝕜E:Type u_2inst✝⁸:NormedAddCommGroup Einst✝⁷:NormedSpace 𝕜 Einst✝⁶:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁵:NormedAddCommGroup Finst✝⁴:NormedSpace 𝕜 Finst✝³:InnerProductSpace' 𝕜 FG:Type u_4inst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace 𝕜 Ginst✝:InnerProductSpace' 𝕜 Gf:E → F × Gf':F × G → Ex:Ehf:HasAdjFDerivAt 𝕜 f f' x⊢ HasAdjoint 𝕜 ⇑(ContinuousLinearMap.snd 𝕜 F G ∘SL fderiv 𝕜 f x) fun dz => f' (0, dz)
    apply HasAdjoint.snd hf.hasAdjoint_fderivAll goals completed! 🐙lemma adjFDeriv_snd [CompleteSpace E] [CompleteSpace F] [CompleteSpace G]
    {f : E → F×G} {x : E} (hf : DifferentiableAt 𝕜 f x) :
    adjFDeriv 𝕜 (fun x => (f x).snd) x = fun dy => adjFDeriv 𝕜 f x (0, dy) := by𝕜:Type u_1inst✝¹²:RCLike 𝕜E:Type u_2inst✝¹¹:NormedAddCommGroup Einst✝¹⁰:NormedSpace 𝕜 Einst✝⁹:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁸:NormedAddCommGroup Finst✝⁷:NormedSpace 𝕜 Finst✝⁶:InnerProductSpace' 𝕜 FG:Type u_4inst✝⁵:NormedAddCommGroup Ginst✝⁴:NormedSpace 𝕜 Ginst✝³:InnerProductSpace' 𝕜 Ginst✝²:CompleteSpace Einst✝¹:CompleteSpace Finst✝:CompleteSpace Gf:E → F × Gx:Ehf:DifferentiableAt 𝕜 f x⊢ adjFDeriv 𝕜 (fun x => (f x).2) x = fun dy => adjFDeriv 𝕜 f x (0, dy)
  apply HasAdjFDerivAt.adjFDeriv𝕜:Type u_1inst✝¹²:RCLike 𝕜E:Type u_2inst✝¹¹:NormedAddCommGroup Einst✝¹⁰:NormedSpace 𝕜 Einst✝⁹:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁸:NormedAddCommGroup Finst✝⁷:NormedSpace 𝕜 Finst✝⁶:InnerProductSpace' 𝕜 FG:Type u_4inst✝⁵:NormedAddCommGroup Ginst✝⁴:NormedSpace 𝕜 Ginst✝³:InnerProductSpace' 𝕜 Ginst✝²:CompleteSpace Einst✝¹:CompleteSpace Finst✝:CompleteSpace Gf:E → F × Gx:Ehf:DifferentiableAt 𝕜 f x⊢ HasAdjFDerivAt 𝕜 (fun x => (f x).2) (fun dy => adjFDeriv 𝕜 f x (0, dy)) x
  apply HasAjdFDerivAt.snd hf.hasAdjFDerivAtAll goals completed! 🐙

@[simp]
lemma adjFDeriv_prod_snd [CompleteSpace E] [CompleteSpace F] {x : F × E} :
    adjFDeriv 𝕜 (Prod.snd : F × E → E) x = fun a => (0, a) := by𝕜:Type u_1inst✝⁸:RCLike 𝕜E:Type u_2inst✝⁷:NormedAddCommGroup Einst✝⁶:NormedSpace 𝕜 Einst✝⁵:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁴:NormedAddCommGroup Finst✝³:NormedSpace 𝕜 Finst✝²:InnerProductSpace' 𝕜 Finst✝¹:CompleteSpace Einst✝:CompleteSpace Fx:F × E⊢ adjFDeriv 𝕜 Prod.snd x = fun a => (0, a)
  change adjFDeriv 𝕜 (fun x => (id x).snd) x = _𝕜:Type u_1inst✝⁸:RCLike 𝕜E:Type u_2inst✝⁷:NormedAddCommGroup Einst✝⁶:NormedSpace 𝕜 Einst✝⁵:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁴:NormedAddCommGroup Finst✝³:NormedSpace 𝕜 Finst✝²:InnerProductSpace' 𝕜 Finst✝¹:CompleteSpace Einst✝:CompleteSpace Fx:F × E⊢ adjFDeriv 𝕜 (fun x => (id x).2) x = fun a => (0, a)
  rw [adjFDeriv_snd𝕜:Type u_1inst✝⁸:RCLike 𝕜E:Type u_2inst✝⁷:NormedAddCommGroup Einst✝⁶:NormedSpace 𝕜 Einst✝⁵:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁴:NormedAddCommGroup Finst✝³:NormedSpace 𝕜 Finst✝²:InnerProductSpace' 𝕜 Finst✝¹:CompleteSpace Einst✝:CompleteSpace Fx:F × E⊢ (fun dy => adjFDeriv 𝕜 id x (0, dy)) = fun a => (0, a)𝕜:Type u_1inst✝⁸:RCLike 𝕜E:Type u_2inst✝⁷:NormedAddCommGroup Einst✝⁶:NormedSpace 𝕜 Einst✝⁵:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁴:NormedAddCommGroup Finst✝³:NormedSpace 𝕜 Finst✝²:InnerProductSpace' 𝕜 Finst✝¹:CompleteSpace Einst✝:CompleteSpace Fx:F × E⊢ DifferentiableAt 𝕜 id x𝕜:Type u_1inst✝⁸:RCLike 𝕜E:Type u_2inst✝⁷:NormedAddCommGroup Einst✝⁶:NormedSpace 𝕜 Einst✝⁵:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁴:NormedAddCommGroup Finst✝³:NormedSpace 𝕜 Finst✝²:InnerProductSpace' 𝕜 Finst✝¹:CompleteSpace Einst✝:CompleteSpace Fx:F × E⊢ (fun dy => adjFDeriv 𝕜 id x (0, dy)) = fun a => (0, a)𝕜:Type u_1inst✝⁸:RCLike 𝕜E:Type u_2inst✝⁷:NormedAddCommGroup Einst✝⁶:NormedSpace 𝕜 Einst✝⁵:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁴:NormedAddCommGroup Finst✝³:NormedSpace 𝕜 Finst✝²:InnerProductSpace' 𝕜 Finst✝¹:CompleteSpace Einst✝:CompleteSpace Fx:F × E⊢ DifferentiableAt 𝕜 id x]𝕜:Type u_1inst✝⁸:RCLike 𝕜E:Type u_2inst✝⁷:NormedAddCommGroup Einst✝⁶:NormedSpace 𝕜 Einst✝⁵:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁴:NormedAddCommGroup Finst✝³:NormedSpace 𝕜 Finst✝²:InnerProductSpace' 𝕜 Finst✝¹:CompleteSpace Einst✝:CompleteSpace Fx:F × E⊢ (fun dy => adjFDeriv 𝕜 id x (0, dy)) = fun a => (0, a)𝕜:Type u_1inst✝⁸:RCLike 𝕜E:Type u_2inst✝⁷:NormedAddCommGroup Einst✝⁶:NormedSpace 𝕜 Einst✝⁵:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁴:NormedAddCommGroup Finst✝³:NormedSpace 𝕜 Finst✝²:InnerProductSpace' 𝕜 Finst✝¹:CompleteSpace Einst✝:CompleteSpace Fx:F × E⊢ DifferentiableAt 𝕜 id x
  funext dy𝕜:Type u_1inst✝⁸:RCLike 𝕜E:Type u_2inst✝⁷:NormedAddCommGroup Einst✝⁶:NormedSpace 𝕜 Einst✝⁵:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁴:NormedAddCommGroup Finst✝³:NormedSpace 𝕜 Finst✝²:InnerProductSpace' 𝕜 Finst✝¹:CompleteSpace Einst✝:CompleteSpace Fx:F × Edy:E⊢ adjFDeriv 𝕜 id x (0, dy) = (0, dy)𝕜:Type u_1inst✝⁸:RCLike 𝕜E:Type u_2inst✝⁷:NormedAddCommGroup Einst✝⁶:NormedSpace 𝕜 Einst✝⁵:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁴:NormedAddCommGroup Finst✝³:NormedSpace 𝕜 Finst✝²:InnerProductSpace' 𝕜 Finst✝¹:CompleteSpace Einst✝:CompleteSpace Fx:F × E⊢ DifferentiableAt 𝕜 id x
  rw [adjFDeriv_id'𝕜:Type u_1inst✝⁸:RCLike 𝕜E:Type u_2inst✝⁷:NormedAddCommGroup Einst✝⁶:NormedSpace 𝕜 Einst✝⁵:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁴:NormedAddCommGroup Finst✝³:NormedSpace 𝕜 Finst✝²:InnerProductSpace' 𝕜 Finst✝¹:CompleteSpace Einst✝:CompleteSpace Fx:F × Edy:E⊢ (fun x dx => dx) x (0, dy) = (0, dy)𝕜:Type u_1inst✝⁸:RCLike 𝕜E:Type u_2inst✝⁷:NormedAddCommGroup Einst✝⁶:NormedSpace 𝕜 Einst✝⁵:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁴:NormedAddCommGroup Finst✝³:NormedSpace 𝕜 Finst✝²:InnerProductSpace' 𝕜 Finst✝¹:CompleteSpace Einst✝:CompleteSpace Fx:F × E⊢ DifferentiableAt 𝕜 id x𝕜:Type u_1inst✝⁸:RCLike 𝕜E:Type u_2inst✝⁷:NormedAddCommGroup Einst✝⁶:NormedSpace 𝕜 Einst✝⁵:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁴:NormedAddCommGroup Finst✝³:NormedSpace 𝕜 Finst✝²:InnerProductSpace' 𝕜 Finst✝¹:CompleteSpace Einst✝:CompleteSpace Fx:F × E⊢ DifferentiableAt 𝕜 id x]𝕜:Type u_1inst✝⁸:RCLike 𝕜E:Type u_2inst✝⁷:NormedAddCommGroup Einst✝⁶:NormedSpace 𝕜 Einst✝⁵:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁴:NormedAddCommGroup Finst✝³:NormedSpace 𝕜 Finst✝²:InnerProductSpace' 𝕜 Finst✝¹:CompleteSpace Einst✝:CompleteSpace Fx:F × E⊢ DifferentiableAt 𝕜 id x
  simpAll goals completed! 🐙lemma hasAdjFDerivAt_uncurry {f : E → F → G} {xy} {fx' fy'}
    (hf : DifferentiableAt 𝕜 (↿f) xy)
    (hfx : HasAdjFDerivAt 𝕜 (f · xy.2) fx' xy.1) (hfy : HasAdjFDerivAt 𝕜 (f xy.1 ·) fy' xy.2) :
    HasAdjFDerivAt 𝕜 (↿f) (fun dz => (fx' dz, fy' dz)) xy where
  differentiableAt :=hf
  hasAdjoint_fderiv := by𝕜:Type u_1inst✝⁹:RCLike 𝕜E:Type u_2inst✝⁸:NormedAddCommGroup Einst✝⁷:NormedSpace 𝕜 Einst✝⁶:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁵:NormedAddCommGroup Finst✝⁴:NormedSpace 𝕜 Finst✝³:InnerProductSpace' 𝕜 FG:Type u_4inst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace 𝕜 Ginst✝:InnerProductSpace' 𝕜 Gf:E → F → Gxy:E × Ffx':G → Efy':G → Fhf:DifferentiableAt 𝕜 (↿f) xyhfx:HasAdjFDerivAt 𝕜 (fun x => f x xy.2) fx' xy.1hfy:HasAdjFDerivAt 𝕜 (fun x => f xy.1 x) fy' xy.2⊢ HasAdjoint 𝕜 ⇑(fderiv 𝕜 (↿f) xy) fun dz => (fx' dz, fy' dz)
    eta_expand𝕜:Type u_1inst✝⁹:RCLike 𝕜E:Type u_2inst✝⁸:NormedAddCommGroup Einst✝⁷:NormedSpace 𝕜 Einst✝⁶:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁵:NormedAddCommGroup Finst✝⁴:NormedSpace 𝕜 Finst✝³:InnerProductSpace' 𝕜 FG:Type u_4inst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace 𝕜 Ginst✝:InnerProductSpace' 𝕜 Gf:E → F → Gxy:E × Ffx':G → Efy':G → Fhf:DifferentiableAt 𝕜 (↿f) xyhfx:HasAdjFDerivAt 𝕜 (fun x => f x xy.2) fx' xy.1hfy:HasAdjFDerivAt 𝕜 (fun x => f xy.1 x) fy' xy.2⊢ HasAdjoint 𝕜 (fun a => (fderiv 𝕜 (fun a => (↿fun a a_1 => f a a_1) a) xy) a) fun dz => (fx' dz, fy' dz)
    simp (disch:=fun_prop) [fderiv_uncurry]𝕜:Type u_1inst✝⁹:RCLike 𝕜E:Type u_2inst✝⁸:NormedAddCommGroup Einst✝⁷:NormedSpace 𝕜 Einst✝⁶:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁵:NormedAddCommGroup Finst✝⁴:NormedSpace 𝕜 Finst✝³:InnerProductSpace' 𝕜 FG:Type u_4inst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace 𝕜 Ginst✝:InnerProductSpace' 𝕜 Gf:E → F → Gxy:E × Ffx':G → Efy':G → Fhf:DifferentiableAt 𝕜 (↿f) xyhfx:HasAdjFDerivAt 𝕜 (fun x => f x xy.2) fx' xy.1hfy:HasAdjFDerivAt 𝕜 (fun x => f xy.1 x) fy' xy.2⊢ HasAdjoint 𝕜 (fun a => (fderiv 𝕜 (fun x => f x xy.2) xy.1) a.1 + (fderiv 𝕜 (fun x => f xy.1 x) xy.2) a.2) fun dz =>
  (fx' dz, fy' dz)
    apply HasAdjoint.congr_adjadjoint𝕜:Type u_1inst✝⁹:RCLike 𝕜E:Type u_2inst✝⁸:NormedAddCommGroup Einst✝⁷:NormedSpace 𝕜 Einst✝⁶:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁵:NormedAddCommGroup Finst✝⁴:NormedSpace 𝕜 Finst✝³:InnerProductSpace' 𝕜 FG:Type u_4inst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace 𝕜 Ginst✝:InnerProductSpace' 𝕜 Gf:E → F → Gxy:E × Ffx':G → Efy':G → Fhf:DifferentiableAt 𝕜 (↿f) xyhfx:HasAdjFDerivAt 𝕜 (fun x => f x xy.2) fx' xy.1hfy:HasAdjFDerivAt 𝕜 (fun x => f xy.1 x) fy' xy.2⊢ HasAdjoint 𝕜 (fun a => (fderiv 𝕜 (fun x => f x xy.2) xy.1) a.1 + (fderiv 𝕜 (fun x => f xy.1 x) xy.2) a.2) ?g'eq𝕜:Type u_1inst✝⁹:RCLike 𝕜E:Type u_2inst✝⁸:NormedAddCommGroup Einst✝⁷:NormedSpace 𝕜 Einst✝⁶:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁵:NormedAddCommGroup Finst✝⁴:NormedSpace 𝕜 Finst✝³:InnerProductSpace' 𝕜 FG:Type u_4inst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace 𝕜 Ginst✝:InnerProductSpace' 𝕜 Gf:E → F → Gxy:E × Ffx':G → Efy':G → Fhf:DifferentiableAt 𝕜 (↿f) xyhfx:HasAdjFDerivAt 𝕜 (fun x => f x xy.2) fx' xy.1hfy:HasAdjFDerivAt 𝕜 (fun x => f xy.1 x) fy' xy.2⊢ ?g' = fun dz => (fx' dz, fy' dz)g'𝕜:Type u_1inst✝⁹:RCLike 𝕜E:Type u_2inst✝⁸:NormedAddCommGroup Einst✝⁷:NormedSpace 𝕜 Einst✝⁶:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁵:NormedAddCommGroup Finst✝⁴:NormedSpace 𝕜 Finst✝³:InnerProductSpace' 𝕜 FG:Type u_4inst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace 𝕜 Ginst✝:InnerProductSpace' 𝕜 Gf:E → F → Gxy:E × Ffx':G → Efy':G → Fhf:DifferentiableAt 𝕜 (↿f) xyhfx:HasAdjFDerivAt 𝕜 (fun x => f x xy.2) fx' xy.1hfy:HasAdjFDerivAt 𝕜 (fun x => f xy.1 x) fy' xy.2⊢ G → E × F
    case adjoint =>𝕜:Type u_1inst✝⁹:RCLike 𝕜E:Type u_2inst✝⁸:NormedAddCommGroup Einst✝⁷:NormedSpace 𝕜 Einst✝⁶:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁵:NormedAddCommGroup Finst✝⁴:NormedSpace 𝕜 Finst✝³:InnerProductSpace' 𝕜 FG:Type u_4inst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace 𝕜 Ginst✝:InnerProductSpace' 𝕜 Gf:E → F → Gxy:E × Ffx':G → Efy':G → Fhf:DifferentiableAt 𝕜 (↿f) xyhfx:HasAdjFDerivAt 𝕜 (fun x => f x xy.2) fx' xy.1hfy:HasAdjFDerivAt 𝕜 (fun x => f xy.1 x) fy' xy.2⊢ HasAdjoint 𝕜 (fun a => (fderiv 𝕜 (fun x => f x xy.2) xy.1) a.1 + (fderiv 𝕜 (fun x => f xy.1 x) xy.2) a.2) ?g'
      apply HasAdjoint.addhf𝕜:Type u_1inst✝⁹:RCLike 𝕜E:Type u_2inst✝⁸:NormedAddCommGroup Einst✝⁷:NormedSpace 𝕜 Einst✝⁶:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁵:NormedAddCommGroup Finst✝⁴:NormedSpace 𝕜 Finst✝³:InnerProductSpace' 𝕜 FG:Type u_4inst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace 𝕜 Ginst✝:InnerProductSpace' 𝕜 Gf:E → F → Gxy:E × Ffx':G → Efy':G → Fhf:DifferentiableAt 𝕜 (↿f) xyhfx:HasAdjFDerivAt 𝕜 (fun x => f x xy.2) fx' xy.1hfy:HasAdjFDerivAt 𝕜 (fun x => f xy.1 x) fy' xy.2⊢ HasAdjoint 𝕜 (fun x => (fderiv 𝕜 (fun x => f x xy.2) xy.1) x.1) ?f'hg𝕜:Type u_1inst✝⁹:RCLike 𝕜E:Type u_2inst✝⁸:NormedAddCommGroup Einst✝⁷:NormedSpace 𝕜 Einst✝⁶:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁵:NormedAddCommGroup Finst✝⁴:NormedSpace 𝕜 Finst✝³:InnerProductSpace' 𝕜 FG:Type u_4inst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace 𝕜 Ginst✝:InnerProductSpace' 𝕜 Gf:E → F → Gxy:E × Ffx':G → Efy':G → Fhf:DifferentiableAt 𝕜 (↿f) xyhfx:HasAdjFDerivAt 𝕜 (fun x => f x xy.2) fx' xy.1hfy:HasAdjFDerivAt 𝕜 (fun x => f xy.1 x) fy' xy.2⊢ HasAdjoint 𝕜 (fun x => (fderiv 𝕜 (fun x => f xy.1 x) xy.2) x.2) ?g'f'𝕜:Type u_1inst✝⁹:RCLike 𝕜E:Type u_2inst✝⁸:NormedAddCommGroup Einst✝⁷:NormedSpace 𝕜 Einst✝⁶:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁵:NormedAddCommGroup Finst✝⁴:NormedSpace 𝕜 Finst✝³:InnerProductSpace' 𝕜 FG:Type u_4inst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace 𝕜 Ginst✝:InnerProductSpace' 𝕜 Gf:E → F → Gxy:E × Ffx':G → Efy':G → Fhf:DifferentiableAt 𝕜 (↿f) xyhfx:HasAdjFDerivAt 𝕜 (fun x => f x xy.2) fx' xy.1hfy:HasAdjFDerivAt 𝕜 (fun x => f xy.1 x) fy' xy.2⊢ G → E × Fg'𝕜:Type u_1inst✝⁹:RCLike 𝕜E:Type u_2inst✝⁸:NormedAddCommGroup Einst✝⁷:NormedSpace 𝕜 Einst✝⁶:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁵:NormedAddCommGroup Finst✝⁴:NormedSpace 𝕜 Finst✝³:InnerProductSpace' 𝕜 FG:Type u_4inst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace 𝕜 Ginst✝:InnerProductSpace' 𝕜 Gf:E → F → Gxy:E × Ffx':G → Efy':G → Fhf:DifferentiableAt 𝕜 (↿f) xyhfx:HasAdjFDerivAt 𝕜 (fun x => f x xy.2) fx' xy.1hfy:HasAdjFDerivAt 𝕜 (fun x => f xy.1 x) fy' xy.2⊢ G → E × F
      apply HasAdjoint.comp (g:=Prod.fst) hfx.hasAdjoint_fderiv (HasAdjoint.fst hasAdjoint_id)hg𝕜:Type u_1inst✝⁹:RCLike 𝕜E:Type u_2inst✝⁸:NormedAddCommGroup Einst✝⁷:NormedSpace 𝕜 Einst✝⁶:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁵:NormedAddCommGroup Finst✝⁴:NormedSpace 𝕜 Finst✝³:InnerProductSpace' 𝕜 FG:Type u_4inst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace 𝕜 Ginst✝:InnerProductSpace' 𝕜 Gf:E → F → Gxy:E × Ffx':G → Efy':G → Fhf:DifferentiableAt 𝕜 (↿f) xyhfx:HasAdjFDerivAt 𝕜 (fun x => f x xy.2) fx' xy.1hfy:HasAdjFDerivAt 𝕜 (fun x => f xy.1 x) fy' xy.2⊢ HasAdjoint 𝕜 (fun x => (fderiv 𝕜 (fun x => f xy.1 x) xy.2) x.2) ?g'g'𝕜:Type u_1inst✝⁹:RCLike 𝕜E:Type u_2inst✝⁸:NormedAddCommGroup Einst✝⁷:NormedSpace 𝕜 Einst✝⁶:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁵:NormedAddCommGroup Finst✝⁴:NormedSpace 𝕜 Finst✝³:InnerProductSpace' 𝕜 FG:Type u_4inst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace 𝕜 Ginst✝:InnerProductSpace' 𝕜 Gf:E → F → Gxy:E × Ffx':G → Efy':G → Fhf:DifferentiableAt 𝕜 (↿f) xyhfx:HasAdjFDerivAt 𝕜 (fun x => f x xy.2) fx' xy.1hfy:HasAdjFDerivAt 𝕜 (fun x => f xy.1 x) fy' xy.2⊢ G → E × F
      apply HasAdjoint.comp (g:=Prod.snd) hfy.hasAdjoint_fderiv (HasAdjoint.snd hasAdjoint_id)All goals completed! 🐙
    case eq =>𝕜:Type u_1inst✝⁹:RCLike 𝕜E:Type u_2inst✝⁸:NormedAddCommGroup Einst✝⁷:NormedSpace 𝕜 Einst✝⁶:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁵:NormedAddCommGroup Finst✝⁴:NormedSpace 𝕜 Finst✝³:InnerProductSpace' 𝕜 FG:Type u_4inst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace 𝕜 Ginst✝:InnerProductSpace' 𝕜 Gf:E → F → Gxy:E × Ffx':G → Efy':G → Fhf:DifferentiableAt 𝕜 (↿f) xyhfx:HasAdjFDerivAt 𝕜 (fun x => f x xy.2) fx' xy.1hfy:HasAdjFDerivAt 𝕜 (fun x => f xy.1 x) fy' xy.2⊢ (fun y => (fx' y, 0) + (0, fy' y)) = fun dz => (fx' dz, fy' dz)
      simpAll goals completed! 🐙lemma adjFDeriv_uncurry [CompleteSpace E] [CompleteSpace F] [CompleteSpace G]
    {f : E → F → G} {xy} (hfx : DifferentiableAt 𝕜 (↿f) xy) :
    adjFDeriv 𝕜 (↿f) xy = fun dz => (adjFDeriv 𝕜 (f · xy.snd) xy.fst dz,
                                    adjFDeriv 𝕜 (f xy.fst ·) xy.snd dz) := by𝕜:Type u_1inst✝¹²:RCLike 𝕜E:Type u_2inst✝¹¹:NormedAddCommGroup Einst✝¹⁰:NormedSpace 𝕜 Einst✝⁹:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁸:NormedAddCommGroup Finst✝⁷:NormedSpace 𝕜 Finst✝⁶:InnerProductSpace' 𝕜 FG:Type u_4inst✝⁵:NormedAddCommGroup Ginst✝⁴:NormedSpace 𝕜 Ginst✝³:InnerProductSpace' 𝕜 Ginst✝²:CompleteSpace Einst✝¹:CompleteSpace Finst✝:CompleteSpace Gf:E → F → Gxy:E × Fhfx:DifferentiableAt 𝕜 (↿f) xy⊢ adjFDeriv 𝕜 (↿f) xy = fun dz => (adjFDeriv 𝕜 (fun x => f x xy.2) xy.1 dz, adjFDeriv 𝕜 (fun x => f xy.1 x) xy.2 dz)
  apply HasAdjFDerivAt.adjFDeriv𝕜:Type u_1inst✝¹²:RCLike 𝕜E:Type u_2inst✝¹¹:NormedAddCommGroup Einst✝¹⁰:NormedSpace 𝕜 Einst✝⁹:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁸:NormedAddCommGroup Finst✝⁷:NormedSpace 𝕜 Finst✝⁶:InnerProductSpace' 𝕜 FG:Type u_4inst✝⁵:NormedAddCommGroup Ginst✝⁴:NormedSpace 𝕜 Ginst✝³:InnerProductSpace' 𝕜 Ginst✝²:CompleteSpace Einst✝¹:CompleteSpace Finst✝:CompleteSpace Gf:E → F → Gxy:E × Fhfx:DifferentiableAt 𝕜 (↿f) xy⊢ HasAdjFDerivAt 𝕜 (↿f) (fun dz => (adjFDeriv 𝕜 (fun x => f x xy.2) xy.1 dz, adjFDeriv 𝕜 (fun x => f xy.1 x) xy.2 dz)) xy
  apply hasAdjFDerivAt_uncurryhf𝕜:Type u_1inst✝¹²:RCLike 𝕜E:Type u_2inst✝¹¹:NormedAddCommGroup Einst✝¹⁰:NormedSpace 𝕜 Einst✝⁹:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁸:NormedAddCommGroup Finst✝⁷:NormedSpace 𝕜 Finst✝⁶:InnerProductSpace' 𝕜 FG:Type u_4inst✝⁵:NormedAddCommGroup Ginst✝⁴:NormedSpace 𝕜 Ginst✝³:InnerProductSpace' 𝕜 Ginst✝²:CompleteSpace Einst✝¹:CompleteSpace Finst✝:CompleteSpace Gf:E → F → Gxy:E × Fhfx:DifferentiableAt 𝕜 (↿f) xy⊢ DifferentiableAt 𝕜 (↿f) xyhfx𝕜:Type u_1inst✝¹²:RCLike 𝕜E:Type u_2inst✝¹¹:NormedAddCommGroup Einst✝¹⁰:NormedSpace 𝕜 Einst✝⁹:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁸:NormedAddCommGroup Finst✝⁷:NormedSpace 𝕜 Finst✝⁶:InnerProductSpace' 𝕜 FG:Type u_4inst✝⁵:NormedAddCommGroup Ginst✝⁴:NormedSpace 𝕜 Ginst✝³:InnerProductSpace' 𝕜 Ginst✝²:CompleteSpace Einst✝¹:CompleteSpace Finst✝:CompleteSpace Gf:E → F → Gxy:E × Fhfx:DifferentiableAt 𝕜 (↿f) xy⊢ HasAdjFDerivAt 𝕜 (fun x => f x xy.2) (adjFDeriv 𝕜 (fun x => f x xy.2) xy.1) xy.1hfy𝕜:Type u_1inst✝¹²:RCLike 𝕜E:Type u_2inst✝¹¹:NormedAddCommGroup Einst✝¹⁰:NormedSpace 𝕜 Einst✝⁹:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁸:NormedAddCommGroup Finst✝⁷:NormedSpace 𝕜 Finst✝⁶:InnerProductSpace' 𝕜 FG:Type u_4inst✝⁵:NormedAddCommGroup Ginst✝⁴:NormedSpace 𝕜 Ginst✝³:InnerProductSpace' 𝕜 Ginst✝²:CompleteSpace Einst✝¹:CompleteSpace Finst✝:CompleteSpace Gf:E → F → Gxy:E × Fhfx:DifferentiableAt 𝕜 (↿f) xy⊢ HasAdjFDerivAt 𝕜 (fun x => f xy.1 x) (adjFDeriv 𝕜 (fun x => f xy.1 x) xy.2) xy.2
  fun_prophfx𝕜:Type u_1inst✝¹²:RCLike 𝕜E:Type u_2inst✝¹¹:NormedAddCommGroup Einst✝¹⁰:NormedSpace 𝕜 Einst✝⁹:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁸:NormedAddCommGroup Finst✝⁷:NormedSpace 𝕜 Finst✝⁶:InnerProductSpace' 𝕜 FG:Type u_4inst✝⁵:NormedAddCommGroup Ginst✝⁴:NormedSpace 𝕜 Ginst✝³:InnerProductSpace' 𝕜 Ginst✝²:CompleteSpace Einst✝¹:CompleteSpace Finst✝:CompleteSpace Gf:E → F → Gxy:E × Fhfx:DifferentiableAt 𝕜 (↿f) xy⊢ HasAdjFDerivAt 𝕜 (fun x => f x xy.2) (adjFDeriv 𝕜 (fun x => f x xy.2) xy.1) xy.1hfy𝕜:Type u_1inst✝¹²:RCLike 𝕜E:Type u_2inst✝¹¹:NormedAddCommGroup Einst✝¹⁰:NormedSpace 𝕜 Einst✝⁹:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁸:NormedAddCommGroup Finst✝⁷:NormedSpace 𝕜 Finst✝⁶:InnerProductSpace' 𝕜 FG:Type u_4inst✝⁵:NormedAddCommGroup Ginst✝⁴:NormedSpace 𝕜 Ginst✝³:InnerProductSpace' 𝕜 Ginst✝²:CompleteSpace Einst✝¹:CompleteSpace Finst✝:CompleteSpace Gf:E → F → Gxy:E × Fhfx:DifferentiableAt 𝕜 (↿f) xy⊢ HasAdjFDerivAt 𝕜 (fun x => f xy.1 x) (adjFDeriv 𝕜 (fun x => f xy.1 x) xy.2) xy.2
  apply DifferentiableAt.hasAdjFDerivAt (by𝕜:Type u_1inst✝¹²:RCLike 𝕜E:Type u_2inst✝¹¹:NormedAddCommGroup Einst✝¹⁰:NormedSpace 𝕜 Einst✝⁹:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁸:NormedAddCommGroup Finst✝⁷:NormedSpace 𝕜 Finst✝⁶:InnerProductSpace' 𝕜 FG:Type u_4inst✝⁵:NormedAddCommGroup Ginst✝⁴:NormedSpace 𝕜 Ginst✝³:InnerProductSpace' 𝕜 Ginst✝²:CompleteSpace Einst✝¹:CompleteSpace Finst✝:CompleteSpace Gf:E → F → Gxy:E × Fhfx:DifferentiableAt 𝕜 (↿f) xy⊢ DifferentiableAt 𝕜 (fun x => f x xy.2) xy.1 fun_propAll goals completed! 🐙)
  apply DifferentiableAt.hasAdjFDerivAt (by𝕜:Type u_1inst✝¹²:RCLike 𝕜E:Type u_2inst✝¹¹:NormedAddCommGroup Einst✝¹⁰:NormedSpace 𝕜 Einst✝⁹:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁸:NormedAddCommGroup Finst✝⁷:NormedSpace 𝕜 Finst✝⁶:InnerProductSpace' 𝕜 FG:Type u_4inst✝⁵:NormedAddCommGroup Ginst✝⁴:NormedSpace 𝕜 Ginst✝³:InnerProductSpace' 𝕜 Ginst✝²:CompleteSpace Einst✝¹:CompleteSpace Finst✝:CompleteSpace Gf:E → F → Gxy:E × Fhfx:DifferentiableAt 𝕜 (↿f) xy⊢ DifferentiableAt 𝕜 (fun x => f xy.1 x) xy.2 fun_propAll goals completed! 🐙)lemma HasAdjFDerivAt.neg {f : E → F} {f'} {x : E} (hf : HasAdjFDerivAt 𝕜 f f' x) :
    HasAdjFDerivAt 𝕜 (fun x => - f x) (fun dy => - f' dy) x where
  differentiableAt := by𝕜:Type u_1inst✝⁶:RCLike 𝕜E:Type u_2inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 Einst✝³:InnerProductSpace' 𝕜 EF:Type u_3inst✝²:NormedAddCommGroup Finst✝¹:NormedSpace 𝕜 Finst✝:InnerProductSpace' 𝕜 Ff:E → Ff':F → Ex:Ehf:HasAdjFDerivAt 𝕜 f f' x⊢ DifferentiableAt 𝕜 (fun x => -f x) x fun_propAll goals completed! 🐙
  hasAdjoint_fderiv := by𝕜:Type u_1inst✝⁶:RCLike 𝕜E:Type u_2inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 Einst✝³:InnerProductSpace' 𝕜 EF:Type u_3inst✝²:NormedAddCommGroup Finst✝¹:NormedSpace 𝕜 Finst✝:InnerProductSpace' 𝕜 Ff:E → Ff':F → Ex:Ehf:HasAdjFDerivAt 𝕜 f f' x⊢ HasAdjoint 𝕜 ⇑(fderiv 𝕜 (fun x => -f x) x) fun dy => -f' dy simp𝕜:Type u_1inst✝⁶:RCLike 𝕜E:Type u_2inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 Einst✝³:InnerProductSpace' 𝕜 EF:Type u_3inst✝²:NormedAddCommGroup Finst✝¹:NormedSpace 𝕜 Finst✝:InnerProductSpace' 𝕜 Ff:E → Ff':F → Ex:Ehf:HasAdjFDerivAt 𝕜 f f' x⊢ HasAdjoint 𝕜 ⇑(-fderiv 𝕜 f x) fun dy => -f' dy; apply hf.hasAdjoint_fderiv.negAll goals completed! 🐙lemma adjFDeriv_neg [CompleteSpace E] [CompleteSpace F]
    {f : E → F} {x : E} (hf : DifferentiableAt 𝕜 f x) :
    adjFDeriv 𝕜 (fun x => - f x) x = fun dy => - adjFDeriv 𝕜 f x dy := by𝕜:Type u_1inst✝⁸:RCLike 𝕜E:Type u_2inst✝⁷:NormedAddCommGroup Einst✝⁶:NormedSpace 𝕜 Einst✝⁵:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁴:NormedAddCommGroup Finst✝³:NormedSpace 𝕜 Finst✝²:InnerProductSpace' 𝕜 Finst✝¹:CompleteSpace Einst✝:CompleteSpace Ff:E → Fx:Ehf:DifferentiableAt 𝕜 f x⊢ adjFDeriv 𝕜 (fun x => -f x) x = fun dy => -adjFDeriv 𝕜 f x dy
  apply HasAdjFDerivAt.adjFDeriv𝕜:Type u_1inst✝⁸:RCLike 𝕜E:Type u_2inst✝⁷:NormedAddCommGroup Einst✝⁶:NormedSpace 𝕜 Einst✝⁵:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁴:NormedAddCommGroup Finst✝³:NormedSpace 𝕜 Finst✝²:InnerProductSpace' 𝕜 Finst✝¹:CompleteSpace Einst✝:CompleteSpace Ff:E → Fx:Ehf:DifferentiableAt 𝕜 f x⊢ HasAdjFDerivAt 𝕜 (fun x => -f x) (fun dy => -adjFDeriv 𝕜 f x dy) x
  apply HasAdjFDerivAt.neg hf.hasAdjFDerivAtAll goals completed! 🐙lemma HasAjdFDerivAt.add {f g : E → F} {f' g'} {x : E}
    (hf : HasAdjFDerivAt 𝕜 f f' x) (hg : HasAdjFDerivAt 𝕜 g g' x) :
    HasAdjFDerivAt 𝕜 (fun x => f x + g x) (fun dy => f' dy + g' dy) x where
  differentiableAt := by𝕜:Type u_1inst✝⁶:RCLike 𝕜E:Type u_2inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 Einst✝³:InnerProductSpace' 𝕜 EF:Type u_3inst✝²:NormedAddCommGroup Finst✝¹:NormedSpace 𝕜 Finst✝:InnerProductSpace' 𝕜 Ff:E → Fg:E → Ff':F → Eg':F → Ex:Ehf:HasAdjFDerivAt 𝕜 f f' xhg:HasAdjFDerivAt 𝕜 g g' x⊢ DifferentiableAt 𝕜 (fun x => f x + g x) x fun_propAll goals completed! 🐙
  hasAdjoint_fderiv := by𝕜:Type u_1inst✝⁶:RCLike 𝕜E:Type u_2inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 Einst✝³:InnerProductSpace' 𝕜 EF:Type u_3inst✝²:NormedAddCommGroup Finst✝¹:NormedSpace 𝕜 Finst✝:InnerProductSpace' 𝕜 Ff:E → Fg:E → Ff':F → Eg':F → Ex:Ehf:HasAdjFDerivAt 𝕜 f f' xhg:HasAdjFDerivAt 𝕜 g g' x⊢ HasAdjoint 𝕜 ⇑(fderiv 𝕜 (fun x => f x + g x) x) fun dy => f' dy + g' dy
    simp (disch:=fun_prop) [fderiv_fun_add]𝕜:Type u_1inst✝⁶:RCLike 𝕜E:Type u_2inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 Einst✝³:InnerProductSpace' 𝕜 EF:Type u_3inst✝²:NormedAddCommGroup Finst✝¹:NormedSpace 𝕜 Finst✝:InnerProductSpace' 𝕜 Ff:E → Fg:E → Ff':F → Eg':F → Ex:Ehf:HasAdjFDerivAt 𝕜 f f' xhg:HasAdjFDerivAt 𝕜 g g' x⊢ HasAdjoint 𝕜 ⇑(fderiv 𝕜 f x + fderiv 𝕜 g x) fun dy => f' dy + g' dy
    apply hf.hasAdjoint_fderiv.add hg.hasAdjoint_fderivAll goals completed! 🐙lemma adjFDeriv_add [CompleteSpace E] [CompleteSpace F]
    {f g : E → F} {x : E}
    (hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g x) :
    adjFDeriv 𝕜 (fun x => f x + g x) x = fun dy => adjFDeriv 𝕜 f x dy + adjFDeriv 𝕜 g x dy := by𝕜:Type u_1inst✝⁸:RCLike 𝕜E:Type u_2inst✝⁷:NormedAddCommGroup Einst✝⁶:NormedSpace 𝕜 Einst✝⁵:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁴:NormedAddCommGroup Finst✝³:NormedSpace 𝕜 Finst✝²:InnerProductSpace' 𝕜 Finst✝¹:CompleteSpace Einst✝:CompleteSpace Ff:E → Fg:E → Fx:Ehf:DifferentiableAt 𝕜 f xhg:DifferentiableAt 𝕜 g x⊢ adjFDeriv 𝕜 (fun x => f x + g x) x = fun dy => adjFDeriv 𝕜 f x dy + adjFDeriv 𝕜 g x dy
  apply HasAdjFDerivAt.adjFDeriv𝕜:Type u_1inst✝⁸:RCLike 𝕜E:Type u_2inst✝⁷:NormedAddCommGroup Einst✝⁶:NormedSpace 𝕜 Einst✝⁵:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁴:NormedAddCommGroup Finst✝³:NormedSpace 𝕜 Finst✝²:InnerProductSpace' 𝕜 Finst✝¹:CompleteSpace Einst✝:CompleteSpace Ff:E → Fg:E → Fx:Ehf:DifferentiableAt 𝕜 f xhg:DifferentiableAt 𝕜 g x⊢ HasAdjFDerivAt 𝕜 (fun x => f x + g x) (fun dy => adjFDeriv 𝕜 f x dy + adjFDeriv 𝕜 g x dy) x
  apply HasAjdFDerivAt.addhf𝕜:Type u_1inst✝⁸:RCLike 𝕜E:Type u_2inst✝⁷:NormedAddCommGroup Einst✝⁶:NormedSpace 𝕜 Einst✝⁵:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁴:NormedAddCommGroup Finst✝³:NormedSpace 𝕜 Finst✝²:InnerProductSpace' 𝕜 Finst✝¹:CompleteSpace Einst✝:CompleteSpace Ff:E → Fg:E → Fx:Ehf:DifferentiableAt 𝕜 f xhg:DifferentiableAt 𝕜 g x⊢ HasAdjFDerivAt 𝕜 f (adjFDeriv 𝕜 f x) xhg𝕜:Type u_1inst✝⁸:RCLike 𝕜E:Type u_2inst✝⁷:NormedAddCommGroup Einst✝⁶:NormedSpace 𝕜 Einst✝⁵:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁴:NormedAddCommGroup Finst✝³:NormedSpace 𝕜 Finst✝²:InnerProductSpace' 𝕜 Finst✝¹:CompleteSpace Einst✝:CompleteSpace Ff:E → Fg:E → Fx:Ehf:DifferentiableAt 𝕜 f xhg:DifferentiableAt 𝕜 g x⊢ HasAdjFDerivAt 𝕜 g (adjFDeriv 𝕜 g x) x
  apply hf.hasAdjFDerivAthg𝕜:Type u_1inst✝⁸:RCLike 𝕜E:Type u_2inst✝⁷:NormedAddCommGroup Einst✝⁶:NormedSpace 𝕜 Einst✝⁵:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁴:NormedAddCommGroup Finst✝³:NormedSpace 𝕜 Finst✝²:InnerProductSpace' 𝕜 Finst✝¹:CompleteSpace Einst✝:CompleteSpace Ff:E → Fg:E → Fx:Ehf:DifferentiableAt 𝕜 f xhg:DifferentiableAt 𝕜 g x⊢ HasAdjFDerivAt 𝕜 g (adjFDeriv 𝕜 g x) x
  apply hg.hasAdjFDerivAtAll goals completed! 🐙lemma HasAdjFDerivAt.sub
    {f g : E → F} {f' g'} {x : E}
    (hf : HasAdjFDerivAt 𝕜 f f' x) (hg : HasAdjFDerivAt 𝕜 g g' x) :
    HasAdjFDerivAt 𝕜 (fun x => f x - g x) (fun dy => f' dy - g' dy) x where
  differentiableAt := by𝕜:Type u_1inst✝⁶:RCLike 𝕜E:Type u_2inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 Einst✝³:InnerProductSpace' 𝕜 EF:Type u_3inst✝²:NormedAddCommGroup Finst✝¹:NormedSpace 𝕜 Finst✝:InnerProductSpace' 𝕜 Ff:E → Fg:E → Ff':F → Eg':F → Ex:Ehf:HasAdjFDerivAt 𝕜 f f' xhg:HasAdjFDerivAt 𝕜 g g' x⊢ DifferentiableAt 𝕜 (fun x => f x - g x) x fun_propAll goals completed! 🐙
  hasAdjoint_fderiv := by𝕜:Type u_1inst✝⁶:RCLike 𝕜E:Type u_2inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 Einst✝³:InnerProductSpace' 𝕜 EF:Type u_3inst✝²:NormedAddCommGroup Finst✝¹:NormedSpace 𝕜 Finst✝:InnerProductSpace' 𝕜 Ff:E → Fg:E → Ff':F → Eg':F → Ex:Ehf:HasAdjFDerivAt 𝕜 f f' xhg:HasAdjFDerivAt 𝕜 g g' x⊢ HasAdjoint 𝕜 ⇑(fderiv 𝕜 (fun x => f x - g x) x) fun dy => f' dy - g' dy
    simp (disch:=fun_prop) [fderiv_fun_sub]𝕜:Type u_1inst✝⁶:RCLike 𝕜E:Type u_2inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 Einst✝³:InnerProductSpace' 𝕜 EF:Type u_3inst✝²:NormedAddCommGroup Finst✝¹:NormedSpace 𝕜 Finst✝:InnerProductSpace' 𝕜 Ff:E → Fg:E → Ff':F → Eg':F → Ex:Ehf:HasAdjFDerivAt 𝕜 f f' xhg:HasAdjFDerivAt 𝕜 g g' x⊢ HasAdjoint 𝕜 ⇑(fderiv 𝕜 f x - fderiv 𝕜 g x) fun dy => f' dy - g' dy
    apply hf.hasAdjoint_fderiv.sub hg.hasAdjoint_fderivAll goals completed! 🐙lemma adjFDeriv_sub [CompleteSpace E] [CompleteSpace F] {f g : E → F} {x : E}
    (hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g x) :
    adjFDeriv 𝕜 (fun x => f x - g x) x = fun dy => adjFDeriv 𝕜 f x dy - adjFDeriv 𝕜 g x dy := by𝕜:Type u_1inst✝⁸:RCLike 𝕜E:Type u_2inst✝⁷:NormedAddCommGroup Einst✝⁶:NormedSpace 𝕜 Einst✝⁵:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁴:NormedAddCommGroup Finst✝³:NormedSpace 𝕜 Finst✝²:InnerProductSpace' 𝕜 Finst✝¹:CompleteSpace Einst✝:CompleteSpace Ff:E → Fg:E → Fx:Ehf:DifferentiableAt 𝕜 f xhg:DifferentiableAt 𝕜 g x⊢ adjFDeriv 𝕜 (fun x => f x - g x) x = fun dy => adjFDeriv 𝕜 f x dy - adjFDeriv 𝕜 g x dy
  apply HasAdjFDerivAt.adjFDeriv𝕜:Type u_1inst✝⁸:RCLike 𝕜E:Type u_2inst✝⁷:NormedAddCommGroup Einst✝⁶:NormedSpace 𝕜 Einst✝⁵:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁴:NormedAddCommGroup Finst✝³:NormedSpace 𝕜 Finst✝²:InnerProductSpace' 𝕜 Finst✝¹:CompleteSpace Einst✝:CompleteSpace Ff:E → Fg:E → Fx:Ehf:DifferentiableAt 𝕜 f xhg:DifferentiableAt 𝕜 g x⊢ HasAdjFDerivAt 𝕜 (fun x => f x - g x) (fun dy => adjFDeriv 𝕜 f x dy - adjFDeriv 𝕜 g x dy) x
  apply HasAdjFDerivAt.subhf𝕜:Type u_1inst✝⁸:RCLike 𝕜E:Type u_2inst✝⁷:NormedAddCommGroup Einst✝⁶:NormedSpace 𝕜 Einst✝⁵:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁴:NormedAddCommGroup Finst✝³:NormedSpace 𝕜 Finst✝²:InnerProductSpace' 𝕜 Finst✝¹:CompleteSpace Einst✝:CompleteSpace Ff:E → Fg:E → Fx:Ehf:DifferentiableAt 𝕜 f xhg:DifferentiableAt 𝕜 g x⊢ HasAdjFDerivAt 𝕜 f (adjFDeriv 𝕜 f x) xhg𝕜:Type u_1inst✝⁸:RCLike 𝕜E:Type u_2inst✝⁷:NormedAddCommGroup Einst✝⁶:NormedSpace 𝕜 Einst✝⁵:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁴:NormedAddCommGroup Finst✝³:NormedSpace 𝕜 Finst✝²:InnerProductSpace' 𝕜 Finst✝¹:CompleteSpace Einst✝:CompleteSpace Ff:E → Fg:E → Fx:Ehf:DifferentiableAt 𝕜 f xhg:DifferentiableAt 𝕜 g x⊢ HasAdjFDerivAt 𝕜 g (adjFDeriv 𝕜 g x) x
  apply hf.hasAdjFDerivAthg𝕜:Type u_1inst✝⁸:RCLike 𝕜E:Type u_2inst✝⁷:NormedAddCommGroup Einst✝⁶:NormedSpace 𝕜 Einst✝⁵:InnerProductSpace' 𝕜 EF:Type u_3inst✝⁴:NormedAddCommGroup Finst✝³:NormedSpace 𝕜 Finst✝²:InnerProductSpace' 𝕜 Finst✝¹:CompleteSpace Einst✝:CompleteSpace Ff:E → Fg:E → Fx:Ehf:DifferentiableAt 𝕜 f xhg:DifferentiableAt 𝕜 g x⊢ HasAdjFDerivAt 𝕜 g (adjFDeriv 𝕜 g x) x
  apply hg.hasAdjFDerivAtAll goals completed! 🐙set_option backward.isDefEq.respectTransparency false in
open InnerProductSpace in
lemma HasAdjFDerivAt.inner {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [InnerProductSpace' ℝ E] (x : E × E) :
    HasAdjFDerivAt ℝ (fun (x : E × E) => ⟪x.1, x.2⟫_ℝ) (fun y => y • (x.2, x.1)) x where
  differentiableAt := byE:Type u_6inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace ℝ Einst✝:InnerProductSpace' ℝ Ex:E × E⊢ DifferentiableAt ℝ (fun x => ⟪x.1, x.2⟫_ℝ) x fun_propAll goals completed! 🐙
  hasAdjoint_fderiv := byE:Type u_6inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace ℝ Einst✝:InnerProductSpace' ℝ Ex:E × E⊢ HasAdjoint ℝ ⇑(fderiv ℝ (fun x => ⟪x.1, x.2⟫_ℝ) x) fun y => y • (x.2, x.1)
    conv =>E:Type u_6inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace ℝ Einst✝:InnerProductSpace' ℝ Ex:E × E| HasAdjoint ℝ ⇑(fderiv ℝ (fun x => ⟪x.1, x.2⟫_ℝ) x) fun y => y • (x.2, x.1)
      enter [2]E:Type u_6inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace ℝ Einst✝:InnerProductSpace' ℝ Ex:E × E| ⇑(fderiv ℝ (fun x => ⟪x.1, x.2⟫_ℝ) x)
      change fun t => fderiv ℝ (fun x => ⟪x.1, x.2⟫_ℝ) x tE:Type u_6inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace ℝ Einst✝:InnerProductSpace' ℝ Ex:E × E| fun t => (fderiv ℝ (fun x => ⟪x.1, x.2⟫_ℝ) x) t
      enter [t]E:Type u_6inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace ℝ Einst✝:InnerProductSpace' ℝ Ex:E × Et:E × E| (fderiv ℝ (fun x => ⟪x.1, x.2⟫_ℝ) x) t
      rw [fderiv_inner_apply' (byE:Type u_6inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace ℝ Einst✝:InnerProductSpace' ℝ Ex:E × Et:E × E⊢ DifferentiableAt ℝ Prod.fst x fun_propAll goals completed! 🐙) (byE:Type u_6inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace ℝ Einst✝:InnerProductSpace' ℝ Ex:E × Et:E × E⊢ DifferentiableAt ℝ Prod.snd x fun_propAll goals completed! 🐙)]
      simp [fderiv_snd, fderiv_fst]E:Type u_6inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace ℝ Einst✝:InnerProductSpace' ℝ Ex:E × Et:E × E| ⟪x.1, t.2⟫_ℝ + ⟪t.1, x.2⟫_ℝ
    constructorE:Type u_6inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace ℝ Einst✝:InnerProductSpace' ℝ Ex:E × E⊢ ∀ (x_1 : E × E) (y : ℝ), ⟪y • (x.2, x.1), x_1⟫_ℝ = ⟪y, ⟪x.1, x_1.2⟫_ℝ + ⟪x_1.1, x.2⟫_ℝ⟫_ℝ
    intro a bE:Type u_6inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace ℝ Einst✝:InnerProductSpace' ℝ Ex:E × Ea:E × Eb:ℝ⊢ ⟪b • (x.2, x.1), a⟫_ℝ = ⟪b, ⟪x.1, a.2⟫_ℝ + ⟪a.1, x.2⟫_ℝ⟫_ℝ
    simp [inner_smul_left']E:Type u_6inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace ℝ Einst✝:InnerProductSpace' ℝ Ex:E × Ea:E × Eb:ℝ⊢ b * ⟪x.2, a.1⟫_ℝ + b * ⟪x.1, a.2⟫_ℝ = (⟪x.1, a.2⟫_ℝ + ⟪a.1, x.2⟫_ℝ) * b
    conv_lhs =>
      enter [1]E:Type u_6inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace ℝ Einst✝:InnerProductSpace' ℝ Ex:E × Ea:E × Eb:ℝ| b * ⟪x.2, a.1⟫_ℝ
      rw [real_inner_comm']E:Type u_6inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace ℝ Einst✝:InnerProductSpace' ℝ Ex:E × Ea:E × Eb:ℝ| b * ⟪a.1, x.2⟫_ℝ
    ringAll goals completed! 🐙