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:

noncomputable def adjFDeriv (𝕜 : Type u_1) [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [InnerProductSpace' 𝕜 F] (f : E → F) (x : E) (dy : F) : E

Adjoint Fréchet derivative

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

The main purpose of this function is to compute gradient f x = adjFDeriv 𝕜 f x 1. We provide easy to use API to compute adjFDeriv.

Equations

• adjFDeriv 𝕜 f x dy = adjoint 𝕜 (⇑(fderiv 𝕜 f x)) dy

structure HasAdjFDerivAt (𝕜 : Type u_1) [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [InnerProductSpace' 𝕜 F] (f : E → F) (f' : F → E) (x : E) : Prop

Function f has adjoint Fréchet derivative f' at x

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

The main purpose is to compute gradient f x = f' 1 = adjFDeriv 𝕜 f x 1.

This structure is analogous to HasFDerivAt and it is often easier to use as theorems for HasAdjFDeriv do not require differentiability assumptions unlike theorems for adjFDeriv.

• differentiableAt : DifferentiableAt 𝕜 f x
• hasAdjoint_fderiv : HasAdjoint 𝕜 (⇑(fderiv 𝕜 f x)) f'

theorem HasAdjFDerivAt.adjFDeriv {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [InnerProductSpace' 𝕜 F] {f : E → F} {f' : F → E} {x : E} (hf : HasAdjFDerivAt 𝕜 f f' x) : adjFDeriv 𝕜 f x = f'

theorem DifferentiableAt.hasAdjFDerivAt {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [InnerProductSpace' 𝕜 F] [CompleteSpace E] [CompleteSpace F] {f : E → F} {x : E} (hf : DifferentiableAt 𝕜 f x) : HasAdjFDerivAt 𝕜 f (adjFDeriv 𝕜 f x) x

theorem ContinuousLinearMap.adjoint.isBoundedBilinearMap_real {X : Type u_6} [NormedAddCommGroup X] [InnerProductSpace ℝ X] [CompleteSpace X] {Y : Type u_7} [NormedAddCommGroup Y] [InnerProductSpace ℝ Y] [CompleteSpace Y] : IsBoundedBilinearMap ℝ fun (fy : (X →L[ℝ] Y) × Y) => (adjoint fy.1) fy.2

theorem HasAdjFDerivAt.contDiffAt_deriv {n : WithTop ℕ∞} {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_7} [NormedAddCommGroup F] [NormedSpace ℝ F] [InnerProductSpace' ℝ F] {G : Type u_8} [NormedAddCommGroup G] [NormedSpace ℝ G] [InnerProductSpace' ℝ G] [CompleteSpace F] [CompleteSpace G] {f : E → F → G} {f' : E → F → G → F} (hf : ∀ (x : E) (y : F), HasAdjFDerivAt ℝ (f x) (f' x y) y) (hf' : ContDiff ℝ (n + 1) ↿f) : ContDiff ℝ n fun (x : E × F × G) => f' x.1 x.2.1 x.2.2

theorem gradient_eq_adjFDeriv {𝕜 : Type u_1} [RCLike 𝕜] {U : Type u_5} [NormedAddCommGroup U] [InnerProductSpace 𝕜 U] [CompleteSpace U] {f : U → 𝕜} {x : U} (hf : DifferentiableAt 𝕜 f x) : gradient f x = adjFDeriv 𝕜 f x 1

theorem hasAdjFDerivAt_id {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] (x : E) : HasAdjFDerivAt 𝕜 (fun (x : E) => x) (fun (dx : E) => dx) x

theorem adjFDeriv_id {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] : (adjFDeriv 𝕜 fun (x : E) => x) = fun (x dx : E) => dx

theorem adjFDeriv_id' {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] : adjFDeriv 𝕜 id = fun (x dx : E) => dx

theorem hasAdjFDerivAt_const {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [InnerProductSpace' 𝕜 F] (x : E) (y : F) : HasAdjFDerivAt 𝕜 (fun (x : E) => y) (fun (x : F) => 0) x

theorem adjFDeriv_const {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [InnerProductSpace' 𝕜 F] (y : F) : (adjFDeriv 𝕜 fun (x : E) => y) = fun (x : E) (x : F) => 0

theorem HasAdjFDerivAt.comp {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [InnerProductSpace' 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] [InnerProductSpace' 𝕜 G] {f : F → G} {g : E → F} {f' : G → F} {g' : F → E} {x : E} (hf : HasAdjFDerivAt 𝕜 f f' (g x)) (hg : HasAdjFDerivAt 𝕜 g g' x) : HasAdjFDerivAt 𝕜 (fun (x : E) => f (g x)) (fun (dz : G) => g' (f' dz)) x

theorem adjFDeriv_comp {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [InnerProductSpace' 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] [InnerProductSpace' 𝕜 G] [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 : E) => f (g x)) x = fun (dy : G) => adjFDeriv 𝕜 g x (adjFDeriv 𝕜 f (g x) dy)

theorem HasAdjFDerivAt.prodMk {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [InnerProductSpace' 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] [InnerProductSpace' 𝕜 G] {f : E → F} {g : E → G} {f' : F → E} {g' : G → E} {x : E} (hf : HasAdjFDerivAt 𝕜 f f' x) (hg : HasAdjFDerivAt 𝕜 g g' x) : HasAdjFDerivAt 𝕜 (fun (x : E) => (f x, g x)) (fun (dyz : F × G) => f' dyz.1 + g' dyz.2) x

theorem HasAjdFDerivAt.fst {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [InnerProductSpace' 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] [InnerProductSpace' 𝕜 G] {f : E → F × G} {f' : F × G → E} {x : E} (hf : HasAdjFDerivAt 𝕜 f f' x) : HasAdjFDerivAt 𝕜 (fun (x : E) => (f x).1) (fun (dy : F) => f' (dy, 0)) x

theorem adjFDeriv_fst {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [InnerProductSpace' 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] [InnerProductSpace' 𝕜 G] [CompleteSpace E] [CompleteSpace F] [CompleteSpace G] {f : E → F × G} {x : E} (hf : DifferentiableAt 𝕜 f x) : adjFDeriv 𝕜 (fun (x : E) => (f x).1) x = fun (dy : F) => adjFDeriv 𝕜 f x (dy, 0)

@[simp]

theorem adjFDeriv_prod_fst {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [InnerProductSpace' 𝕜 F] [CompleteSpace E] [CompleteSpace F] {x : F × E} : adjFDeriv 𝕜 Prod.fst x = fun (a : F) => (a, 0)

theorem HasAjdFDerivAt.snd {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [InnerProductSpace' 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] [InnerProductSpace' 𝕜 G] {f : E → F × G} {f' : F × G → E} {x : E} (hf : HasAdjFDerivAt 𝕜 f f' x) : HasAdjFDerivAt 𝕜 (fun (x : E) => (f x).2) (fun (dz : G) => f' (0, dz)) x

theorem adjFDeriv_snd {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [InnerProductSpace' 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] [InnerProductSpace' 𝕜 G] [CompleteSpace E] [CompleteSpace F] [CompleteSpace G] {f : E → F × G} {x : E} (hf : DifferentiableAt 𝕜 f x) : adjFDeriv 𝕜 (fun (x : E) => (f x).2) x = fun (dy : G) => adjFDeriv 𝕜 f x (0, dy)

@[simp]

theorem adjFDeriv_prod_snd {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [InnerProductSpace' 𝕜 F] [CompleteSpace E] [CompleteSpace F] {x : F × E} : adjFDeriv 𝕜 Prod.snd x = fun (a : E) => (0, a)

theorem hasAdjFDerivAt_uncurry {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [InnerProductSpace' 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] [InnerProductSpace' 𝕜 G] {f : E → F → G} {xy : E × F} {fx' : G → E} {fy' : G → F} (hf : DifferentiableAt 𝕜 (↿f) xy) (hfx : HasAdjFDerivAt 𝕜 (fun (x : E) => f x xy.2) fx' xy.1) (hfy : HasAdjFDerivAt 𝕜 (fun (x : F) => f xy.1 x) fy' xy.2) : HasAdjFDerivAt 𝕜 (↿f) (fun (dz : G) => (fx' dz, fy' dz)) xy

theorem adjFDeriv_uncurry {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [InnerProductSpace' 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] [InnerProductSpace' 𝕜 G] [CompleteSpace E] [CompleteSpace F] [CompleteSpace G] {f : E → F → G} {xy : E × F} (hfx : DifferentiableAt 𝕜 (↿f) xy) : adjFDeriv 𝕜 (↿f) xy = fun (dz : G) => (adjFDeriv 𝕜 (fun (x : E) => f x xy.2) xy.1 dz, adjFDeriv 𝕜 (fun (x : F) => f xy.1 x) xy.2 dz)

theorem HasAdjFDerivAt.neg {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [InnerProductSpace' 𝕜 F] {f : E → F} {f' : F → E} {x : E} (hf : HasAdjFDerivAt 𝕜 f f' x) : HasAdjFDerivAt 𝕜 (fun (x : E) => -f x) (fun (dy : F) => -f' dy) x

theorem adjFDeriv_neg {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [InnerProductSpace' 𝕜 F] [CompleteSpace E] [CompleteSpace F] {f : E → F} {x : E} (hf : DifferentiableAt 𝕜 f x) : adjFDeriv 𝕜 (fun (x : E) => -f x) x = fun (dy : F) => -adjFDeriv 𝕜 f x dy

theorem HasAjdFDerivAt.add {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [InnerProductSpace' 𝕜 F] {f g : E → F} {f' g' : F → E} {x : E} (hf : HasAdjFDerivAt 𝕜 f f' x) (hg : HasAdjFDerivAt 𝕜 g g' x) : HasAdjFDerivAt 𝕜 (fun (x : E) => f x + g x) (fun (dy : F) => f' dy + g' dy) x

theorem adjFDeriv_add {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [InnerProductSpace' 𝕜 F] [CompleteSpace E] [CompleteSpace F] {f g : E → F} {x : E} (hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g x) : adjFDeriv 𝕜 (fun (x : E) => f x + g x) x = fun (dy : F) => adjFDeriv 𝕜 f x dy + adjFDeriv 𝕜 g x dy

theorem HasAdjFDerivAt.sub {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [InnerProductSpace' 𝕜 F] {f g : E → F} {f' g' : F → E} {x : E} (hf : HasAdjFDerivAt 𝕜 f f' x) (hg : HasAdjFDerivAt 𝕜 g g' x) : HasAdjFDerivAt 𝕜 (fun (x : E) => f x - g x) (fun (dy : F) => f' dy - g' dy) x

theorem adjFDeriv_sub {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [InnerProductSpace' 𝕜 F] [CompleteSpace E] [CompleteSpace F] {f g : E → F} {x : E} (hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g x) : adjFDeriv 𝕜 (fun (x : E) => f x - g x) x = fun (dy : F) => adjFDeriv 𝕜 f x dy - adjFDeriv 𝕜 g x dy

theorem HasAdjFDerivAt.smul {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [InnerProductSpace' 𝕜 F] {x : E} {f : E → F} {g : E → 𝕜} {f' : F → E} {g' : 𝕜 → E} (hf : HasAdjFDerivAt 𝕜 f f' x) (hg : HasAdjFDerivAt 𝕜 g g' x) : HasAdjFDerivAt 𝕜 (fun (x : E) => g x • f x) (fun (dy : F) => (starRingEnd 𝕜) (g x) • f' dy + g' ((starRingEnd 𝕜) (Inner.inner 𝕜 dy (f x)))) x

theorem adjFDeriv_smul {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [InnerProductSpace' 𝕜 F] [CompleteSpace E] [CompleteSpace F] {f : E → F} {g : E → 𝕜} {x : E} (hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g x) : adjFDeriv 𝕜 (fun (x : E) => g x • f x) x = fun (dy : F) => (starRingEnd 𝕜) (g x) • adjFDeriv 𝕜 f x dy + adjFDeriv 𝕜 g x ((starRingEnd 𝕜) (inner 𝕜 dy (f x)))

theorem HasAdjFDerivAt.inner {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [InnerProductSpace' ℝ E] (x : E × E) : HasAdjFDerivAt ℝ (fun (x : E × E) => Inner.inner ℝ x.1 x.2) (fun (y : ℝ) => y • (x.2, x.1)) x

theorem adjFDeriv_inner {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [InnerProductSpace' ℝ E] (x : E × E) : adjFDeriv ℝ (fun (x : E × E) => inner ℝ x.1 x.2) x = fun (y : ℝ) => y • (x.2, x.1)