duality between gradient and directional derivative

Stream: new members

[Johannes Riesterer]

Hello. I need help to prove the duality between gradient and directional derivative.

-- Definition der Richtungsableitung
def directional_deriv (f : F → ℝ) (x : F) (v : F) : ℝ :=
  (fderiv ℝ f x) v
-- Beweis, dass die Richtungsableitung gleich dem inneren Produkt des Gradienten mit dem Vektor ist
theorem directional_deriv_eq_inner_product:
  directional_deriv f x v = ⟪gradient f x, v⟫ :=
by
  rw [directional_deriv, gradient]
  sorry

Thanx for any help

[Notification Bot]

A message was moved here from #new members > Help with simple proof by Ruben Van de Velde.

[Ruben Van de Velde]

Please provide a #mwe, but probably the next question is "what's the proof in English?"

[Johannes Riesterer]

I want to prove that the gradient points into the direction of the steepest ascend. This part is missing. Here is my code:

import Mathlib.Analysis.InnerProductSpace.Dual
import Mathlib.Analysis.Calculus.FDeriv.Basic
import Mathlib.Analysis.Calculus.Deriv.Basic
import Mathlib.Analysis.Calculus.Gradient.Basic

open Topology InnerProductSpace Set Filter Real

noncomputable section

variable {𝕜 F : Type*} [RCLike 𝕜]
variable [NormedAddCommGroup F] [InnerProductSpace  ℝ F] [CompleteSpace F]
variable {f : F →  ℝ} {f' x : F}
local notation "⟪" x ", " y "⟫" => @inner ℝ _ _ x y
scoped[Gradient] notation "∇" => gradient
-- Beweis, dass der Gradient in die Richtung des steilsten Anstiegs zeigt
theorem gradient_csu (hf : DifferentiableAt  ℝ f x) (v : F) :
⟪gradient f x, v⟫ * ⟪gradient f x, v⟫  ≤ ⟪gradient f x, gradient f x⟫ *  ⟪v, v⟫ :=
by
  exact real_inner_mul_inner_self_le (gradient f x) v
-- Definition der Richtungsableitung
def directional_deriv (f : F → ℝ) (x : F) (v : F) : ℝ :=
  (fderiv ℝ f x) v
-- Beweis, dass die Richtungsableitung gleich dem inneren Produkt des Gradienten mit dem Vektor ist
theorem directional_deriv_eq_inner_product:
  directional_deriv f x v = ⟪gradient f x, v⟫ :=
by
  rw [directional_deriv, gradient]
  sorry
-- Beweis, dass der Gradient in die Richtung des steilsten Anstiegs zeigt
theorem gradient_max_directional_deriv (hf : DifferentiableAt ℝ f x) (v : F) :
directional_deriv f x v ≤ ‖gradient f x‖ * ‖v‖ :=
by
  rw [directional_deriv_eq_inner_product]
  exact real_inner_le_norm (gradient f x) v

[Richard Copley]

rw? says rw [toDual_symm_apply].

[Johannes Riesterer]

That works. Thank you very much Richard