Mathlib.Analysis.Calculus.FDeriv.Bilinear

IsBoundedBilinearMap.hasStrictFDerivAt theorem

(h : IsBoundedBilinearMap 𝕜 b) (p : E × F) : HasStrictFDerivAt b (h.deriv p) p

Full source

@[fun_prop]
theorem IsBoundedBilinearMap.hasStrictFDerivAt (h : IsBoundedBilinearMap 𝕜 b) (p : E × F) :
    HasStrictFDerivAt b (h.deriv p) p := by
  simp only [hasStrictFDerivAt_iff_isLittleO]
  simp only [← map_add_left_nhds_zero (p, p), isLittleO_map]
  set T := (E × F) × E × F
  calc
    _ = fun x ↦ h.deriv (x.1 - x.2) (x.2.1, x.1.2) := by
      ext ⟨⟨x₁, y₁⟩, ⟨x₂, y₂⟩⟩
      rcases p with ⟨x, y⟩
      simp only [map_sub, deriv_apply, Function.comp_apply, Prod.mk_add_mk, h.add_right, h.add_left,
        Prod.mk_sub_mk, h.map_sub_left, h.map_sub_right, sub_add_sub_cancel]
      abel
    -- _ =O[𝓝 (0 : T)] fun x ↦ ‖x.1 - x.2‖ * ‖(x.2.1, x.1.2)‖ :=
    --     h.toContinuousLinearMap.deriv₂.isBoundedBilinearMap.isBigO_comp
    -- _ = o[𝓝 0] fun x ↦ ‖x.1 - x.2‖ * 1 := _
    _ =o[𝓝 (0 : T)] fun x ↦ x.1 - x.2 := by
      -- TODO : add 2 `calc` steps instead of the next 3 lines
      refine h.toContinuousLinearMap.deriv₂.isBoundedBilinearMap.isBigO_comp.trans_isLittleO ?_
      suffices (fun x : T ↦ ‖x.1 - x.2‖ * ‖(x.2.1, x.1.2)‖) =o[𝓝 0] fun x ↦ ‖x.1 - x.2‖ * 1 by
        simpa only [mul_one, isLittleO_norm_right] using this
      refine (isBigO_refl _ _).mul_isLittleO ((isLittleO_one_iff _).2 ?_)
      -- TODO: `continuity` fails
      exact (continuous_snd.fst.prodMk continuous_fst.snd).norm.tendsto' _ _ (by simp)
    _ = _ := by simp [T, Function.comp_def]

Strict Fréchet Differentiability of Bounded Bilinear Maps

Informal description

Let $E$, $F$, and $G$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $b : E \times F \to G$ be a bounded bilinear map. Then for any point $p \in E \times F$, the map $b$ has a strict Fréchet derivative at $p$ given by the continuous linear map $(x, y) \mapsto b(x, p.2) + b(p.1, y)$.

IsBoundedBilinearMap.hasFDerivAt theorem

(h : IsBoundedBilinearMap 𝕜 b) (p : E × F) : HasFDerivAt b (h.deriv p) p

Full source

@[fun_prop]
theorem IsBoundedBilinearMap.hasFDerivAt (h : IsBoundedBilinearMap 𝕜 b) (p : E × F) :
    HasFDerivAt b (h.deriv p) p :=
  (h.hasStrictFDerivAt p).hasFDerivAt

Fréchet Differentiability of Bounded Bilinear Maps

Informal description

Let $E$, $F$, and $G$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $b : E \times F \to G$ be a bounded bilinear map. Then for any point $p \in E \times F$, the map $b$ has a Fréchet derivative at $p$ given by the continuous linear map $(x, y) \mapsto b(x, p_2) + b(p_1, y)$, where $p = (p_1, p_2)$.

IsBoundedBilinearMap.hasFDerivWithinAt theorem

(h : IsBoundedBilinearMap 𝕜 b) (p : E × F) : HasFDerivWithinAt b (h.deriv p) u p

Full source

@[fun_prop]
theorem IsBoundedBilinearMap.hasFDerivWithinAt (h : IsBoundedBilinearMap 𝕜 b) (p : E × F) :
    HasFDerivWithinAt b (h.deriv p) u p :=
  (h.hasFDerivAt p).hasFDerivWithinAt

Fréchet Differentiability of Bounded Bilinear Maps Within a Subset

Informal description

Let $E$, $F$, and $G$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $b : E \times F \to G$ be a bounded bilinear map. For any point $p \in E \times F$ and any subset $u \subseteq E \times F$, the map $b$ has a Fréchet derivative at $p$ within $u$ given by the continuous linear map $(x, y) \mapsto b(x, p_2) + b(p_1, y)$, where $p = (p_1, p_2)$.

IsBoundedBilinearMap.differentiableAt theorem

(h : IsBoundedBilinearMap 𝕜 b) (p : E × F) : DifferentiableAt 𝕜 b p

Full source

@[fun_prop]
theorem IsBoundedBilinearMap.differentiableAt (h : IsBoundedBilinearMap 𝕜 b) (p : E × F) :
    DifferentiableAt 𝕜 b p :=
  (h.hasFDerivAt p).differentiableAt

Differentiability of Bounded Bilinear Maps

Informal description

Let $E$, $F$, and $G$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $b : E \times F \to G$ be a bounded bilinear map. Then for any point $p \in E \times F$, the map $b$ is differentiable at $p$.

IsBoundedBilinearMap.differentiableWithinAt theorem

(h : IsBoundedBilinearMap 𝕜 b) (p : E × F) : DifferentiableWithinAt 𝕜 b u p

Full source

@[fun_prop]
theorem IsBoundedBilinearMap.differentiableWithinAt (h : IsBoundedBilinearMap 𝕜 b) (p : E × F) :
    DifferentiableWithinAt 𝕜 b u p :=
  (h.differentiableAt p).differentiableWithinAt

Differentiability of Bounded Bilinear Maps Within a Subset

Informal description

Let $E$, $F$, and $G$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $b : E \times F \to G$ be a bounded bilinear map. Then for any point $p \in E \times F$ and any subset $u \subseteq E \times F$, the map $b$ is differentiable at $p$ within $u$.

IsBoundedBilinearMap.fderiv theorem

(h : IsBoundedBilinearMap 𝕜 b) (p : E × F) : fderiv 𝕜 b p = h.deriv p

Full source

protected theorem IsBoundedBilinearMap.fderiv (h : IsBoundedBilinearMap 𝕜 b) (p : E × F) :
    fderiv 𝕜 b p = h.deriv p :=
  HasFDerivAt.fderiv (h.hasFDerivAt p)

Fréchet Derivative Formula for Bounded Bilinear Maps

Informal description

Let $E$, $F$, and $G$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $b : E \times F \to G$ be a bounded bilinear map. For any point $p = (p_1, p_2) \in E \times F$, the Fréchet derivative of $b$ at $p$ is given by the continuous linear map $(x, y) \mapsto b(x, p_2) + b(p_1, y)$.

IsBoundedBilinearMap.fderivWithin theorem

 (h : IsBoundedBilinearMap 𝕜 b) (p : E × F) (hxs : UniqueDiffWithinAt 𝕜 u p) : fderivWithin 𝕜 b u p = h.deriv p

Full source

protected theorem IsBoundedBilinearMap.fderivWithin (h : IsBoundedBilinearMap 𝕜 b) (p : E × F)
    (hxs : UniqueDiffWithinAt 𝕜 u p) : fderivWithin 𝕜 b u p = h.deriv p := by
  rw [DifferentiableAt.fderivWithin (h.differentiableAt p) hxs]
  exact h.fderiv p

Fréchet Derivative Formula for Bounded Bilinear Maps Within a Subset

Informal description

Let $E$, $F$, and $G$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $b : E \times F \to G$ be a bounded bilinear map. For any point $p = (p_1, p_2) \in E \times F$ and subset $u \subseteq E \times F$ that is uniquely differentiable at $p$, the Fréchet derivative of $b$ at $p$ within $u$ is given by the continuous linear map $(x, y) \mapsto b(x, p_2) + b(p_1, y)$.

IsBoundedBilinearMap.differentiable theorem

(h : IsBoundedBilinearMap 𝕜 b) : Differentiable 𝕜 b

Full source

@[fun_prop]
theorem IsBoundedBilinearMap.differentiable (h : IsBoundedBilinearMap 𝕜 b) : Differentiable 𝕜 b :=
  fun x => h.differentiableAt x

Differentiability of Bounded Bilinear Maps

Informal description

Let $E$, $F$, and $G$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $b : E \times F \to G$ be a bounded bilinear map. Then $b$ is differentiable everywhere on $E \times F$.

IsBoundedBilinearMap.differentiableOn theorem

(h : IsBoundedBilinearMap 𝕜 b) : DifferentiableOn 𝕜 b u

Full source

@[fun_prop]
theorem IsBoundedBilinearMap.differentiableOn (h : IsBoundedBilinearMap 𝕜 b) :
    DifferentiableOn 𝕜 b u :=
  h.differentiable.differentiableOn

Differentiability of Bounded Bilinear Maps on Subsets

Informal description

Let $E$, $F$, and $G$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $b : E \times F \to G$ be a bounded bilinear map. Then for any subset $u \subseteq E \times F$, the map $b$ is differentiable on $u$.

ContinuousLinearMap.hasFDerivWithinAt_of_bilinear theorem

 {f : G' → E} {g : G' → F} {f' : G' →L[𝕜] E} {g' : G' →L[𝕜] F} {x : G'} {s : Set G'} (hf : HasFDerivWithinAt f f' s x)
  (hg : HasFDerivWithinAt g g' s x) :
  HasFDerivWithinAt (fun y => B (f y) (g y)) (B.precompR G' (f x) g' + B.precompL G' f' (g x)) s x

Full source

@[fun_prop]
theorem ContinuousLinearMap.hasFDerivWithinAt_of_bilinear {f : G' → E} {g : G' → F}
    {f' : G' →L[𝕜] E} {g' : G' →L[𝕜] F} {x : G'} {s : Set G'} (hf : HasFDerivWithinAt f f' s x)
    (hg : HasFDerivWithinAt g g' s x) :
    HasFDerivWithinAt (fun y => B (f y) (g y))
      (B.precompR G' (f x) g' + B.precompL G' f' (g x)) s x := by
  exact (B.isBoundedBilinearMap.hasFDerivAt (f x, g x)).comp_hasFDerivWithinAt x (hf.prodMk hg)

Fréchet Differentiability of Bilinear Composition Within a Set

Informal description

Let $E$, $F$, $G$, and $G'$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $B : E \times F \to G$ be a continuous bilinear map. Given functions $f : G' \to E$ and $g : G' \to F$ that are Fréchet differentiable within a set $s \subseteq G'$ at a point $x \in s$ with derivatives $f' : G' \toL[\mathbb{K}] E$ and $g' : G' \toL[\mathbb{K}] F$ respectively, the function $y \mapsto B(f(y), g(y))$ is Fréchet differentiable within $s$ at $x$ with derivative given by the sum of the bilinear maps $B(\cdot, g(x)) \circ f'$ and $B(f(x), \cdot) \circ g'$.

ContinuousLinearMap.hasFDerivAt_of_bilinear theorem

 {f : G' → E} {g : G' → F} {f' : G' →L[𝕜] E} {g' : G' →L[𝕜] F} {x : G'} (hf : HasFDerivAt f f' x)
  (hg : HasFDerivAt g g' x) : HasFDerivAt (fun y => B (f y) (g y)) (B.precompR G' (f x) g' + B.precompL G' f' (g x)) x

Full source

@[fun_prop]
theorem ContinuousLinearMap.hasFDerivAt_of_bilinear {f : G' → E} {g : G' → F} {f' : G' →L[𝕜] E}
    {g' : G' →L[𝕜] F} {x : G'} (hf : HasFDerivAt f f' x) (hg : HasFDerivAt g g' x) :
    HasFDerivAt (fun y => B (f y) (g y)) (B.precompR G' (f x) g' + B.precompL G' f' (g x)) x := by
  exact (B.isBoundedBilinearMap.hasFDerivAt (f x, g x)).comp x (hf.prodMk hg)

Differentiability of Bilinear Composition at a Point

Informal description

Let $E$, $F$, $G$, and $G'$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $B : E \times F \to G$ be a continuous bilinear map. Given functions $f : G' \to E$ and $g : G' \to F$ that are Fréchet differentiable at $x \in G'$ with derivatives $f'$ and $g'$ respectively, the function $y \mapsto B(f(y), g(y))$ is Fréchet differentiable at $x$ with derivative given by: \[ B(f(x), g') + B(f', g(x)) \] where $B(f(x), \cdot)$ and $B(\cdot, g(x))$ denote the linear maps obtained by fixing the first and second arguments of $B$ respectively.

ContinuousLinearMap.hasStrictFDerivAt_of_bilinear theorem

 {f : G' → E} {g : G' → F} {f' : G' →L[𝕜] E} {g' : G' →L[𝕜] F} {x : G'} (hf : HasStrictFDerivAt f f' x)
  (hg : HasStrictFDerivAt g g' x) :
  HasStrictFDerivAt (fun y => B (f y) (g y)) (B.precompR G' (f x) g' + B.precompL G' f' (g x)) x

Full source

@[fun_prop]
theorem ContinuousLinearMap.hasStrictFDerivAt_of_bilinear
    {f : G' → E} {g : G' → F} {f' : G' →L[𝕜] E}
    {g' : G' →L[𝕜] F} {x : G'} (hf : HasStrictFDerivAt f f' x) (hg : HasStrictFDerivAt g g' x) :
    HasStrictFDerivAt (fun y => B (f y) (g y))
      (B.precompR G' (f x) g' + B.precompL G' f' (g x)) x :=
  (B.isBoundedBilinearMap.hasStrictFDerivAt (f x, g x)).comp x (hf.prodMk hg)

Strict Fréchet Differentiability of Bilinear Composition at a Point

Informal description

Let $E$, $F$, $G$, and $G'$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $B : E \times F \to G$ be a continuous bilinear map. Given functions $f : G' \to E$ and $g : G' \to F$ that are strictly Fréchet differentiable at $x \in G'$ with derivatives $f' : G' \toL[\mathbb{K}] E$ and $g' : G' \toL[\mathbb{K}] F$ respectively, the function $y \mapsto B(f(y), g(y))$ is strictly Fréchet differentiable at $x$ with derivative given by: \[ B(f(x), g') + B(f', g(x)) \] where $B(f(x), \cdot)$ and $B(\cdot, g(x))$ denote the linear maps obtained by fixing the first and second arguments of $B$ respectively.

ContinuousLinearMap.fderivWithin_of_bilinear theorem

 {f : G' → E} {g : G' → F} {x : G'} {s : Set G'} (hf : DifferentiableWithinAt 𝕜 f s x)
  (hg : DifferentiableWithinAt 𝕜 g s x) (hs : UniqueDiffWithinAt 𝕜 s x) :
  fderivWithin 𝕜 (fun y => B (f y) (g y)) s x =
    B.precompR G' (f x) (fderivWithin 𝕜 g s x) + B.precompL G' (fderivWithin 𝕜 f s x) (g x)

Full source

theorem ContinuousLinearMap.fderivWithin_of_bilinear {f : G' → E} {g : G' → F} {x : G'} {s : Set G'}
    (hf : DifferentiableWithinAt 𝕜 f s x) (hg : DifferentiableWithinAt 𝕜 g s x)
    (hs : UniqueDiffWithinAt 𝕜 s x) :
    fderivWithin 𝕜 (fun y => B (f y) (g y)) s x =
      B.precompR G' (f x) (fderivWithin 𝕜 g s x) + B.precompL G' (fderivWithin 𝕜 f s x) (g x) :=
  (B.hasFDerivWithinAt_of_bilinear hf.hasFDerivWithinAt hg.hasFDerivWithinAt).fderivWithin hs

Fréchet derivative of a bilinear composition within a set

Informal description

Let $E$, $F$, $G$, and $G'$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $B : E \times F \to G$ be a continuous bilinear map. Given functions $f : G' \to E$ and $g : G' \to F$ that are differentiable within a set $s \subseteq G'$ at a point $x \in s$, and assuming $s$ is uniquely differentiable at $x$, the Fréchet derivative of the function $y \mapsto B(f(y), g(y))$ within $s$ at $x$ is given by: \[ B(f(x), \cdot) \circ g'(x) + B(\cdot, g(x)) \circ f'(x) \] where $f'(x)$ and $g'(x)$ are the Fréchet derivatives of $f$ and $g$ within $s$ at $x$, respectively.

ContinuousLinearMap.fderiv_of_bilinear theorem

 {f : G' → E} {g : G' → F} {x : G'} (hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g x) :
  fderiv 𝕜 (fun y => B (f y) (g y)) x = B.precompR G' (f x) (fderiv 𝕜 g x) + B.precompL G' (fderiv 𝕜 f x) (g x)

Full source

theorem ContinuousLinearMap.fderiv_of_bilinear {f : G' → E} {g : G' → F} {x : G'}
    (hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g x) :
    fderiv 𝕜 (fun y => B (f y) (g y)) x =
      B.precompR G' (f x) (fderiv 𝕜 g x) + B.precompL G' (fderiv 𝕜 f x) (g x) :=
  (B.hasFDerivAt_of_bilinear hf.hasFDerivAt hg.hasFDerivAt).fderiv

Fréchet Derivative of a Bilinear Composition: $fderiv_{\mathbb{K}} (B \circ (f,g)) = B(f, g') + B(f', g)$

Informal description

Let $E$, $F$, $G$, and $G'$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $B : E \times F \to G$ be a continuous bilinear map. Given functions $f : G' \to E$ and $g : G' \to F$ that are Fréchet differentiable at a point $x \in G'$, the Fréchet derivative of the function $y \mapsto B(f(y), g(y))$ at $x$ is given by: \[ B(f(x), g'(x)) + B(f'(x), g(x)) \] where $f'(x)$ and $g'(x)$ are the Fréchet derivatives of $f$ and $g$ at $x$ respectively.