def HasRadialSegmentsAt {H : Type u} [NormedAddCommGroup H] [NormedSpace ℝ H] (C : Set H) (x : H) : Prop

A set C admits short positive line segments from x in every direction.

def HasGateauxDerivativeWithinAt {H : Type u} {K : Type v} [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup K] [NormedSpace ℝ K] (T : H → K) (A : H →L[ℝ] K) (C : Set H) (x : H) : Prop

Definition 2.54: A is the Gâteaux derivative of T at x within C if every direction from x stays in C along some short positive segment and the restriction of T to each affine line through x has the one-sided derivative A y at 0.

@[reducible, inline]

abbrev HasGateauxDerivativeAt {H : Type u} {K : Type v} [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup K] [NormedSpace ℝ K] (T : H → K) (A : H →L[ℝ] K) (x : H) : Prop

T has Gâteaux derivative A at x if it has this derivative within the whole space.

@[reducible, inline]

abbrev GateauxDifferentiableWithinAt {H : Type u} {K : Type v} [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup K] [NormedSpace ℝ K] (T : H → K) (C : Set H) (x : H) : Prop

T is Gâteaux differentiable within C at x if it admits some Gâteaux derivative there.

@[reducible, inline]

abbrev GateauxDifferentiableAt {H : Type u} {K : Type v} [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup K] [NormedSpace ℝ K] (T : H → K) (x : H) : Prop

T is Gâteaux differentiable at x if it is Gâteaux differentiable within the whole space.

def GateauxDifferentiableOn {H : Type u} {K : Type v} [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup K] [NormedSpace ℝ K] (T : H → K) (C : Set H) : Prop

T is Gâteaux differentiable on C if it is Gâteaux differentiable at every point of C.

def HasGateauxDerivativeOn {H : Type u} {K : Type v} [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup K] [NormedSpace ℝ K] (T : H → K) (DT : H → H →L[ℝ] K) (C : Set H) : Prop

A derivative field DT on C assigns to each point of C a Gâteaux derivative of T.

def HasGateauxSecondDerivativeWithinAt {H : Type u} {K : Type v} [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup K] [NormedSpace ℝ K] (T : H → K) (DT : H → H →L[ℝ] K) (C : Set H) (x : H) (A₂ : H →L[ℝ] H →L[ℝ] K) : Prop

Definition 2.54: relative to a first-derivative field DT, A₂ is a second Gâteaux derivative of T at x within C if DT x is a Gâteaux derivative of T at x within C and the operator field DT has Gâteaux derivative A₂ there.

theorem HasRadialSegmentsAt.of_mem_nhds {H : Type u} [NormedAddCommGroup H] [NormedSpace ℝ H] {C : Set H} {x : H} (hC : C ∈ nhds x) : HasRadialSegmentsAt C x

A neighborhood of x contains a short positive line segment from x in every direction.

theorem hasRadialSegmentsAt_univ {H : Type u} [NormedAddCommGroup H] [NormedSpace ℝ H] (x : H) : HasRadialSegmentsAt Set.univ x

Helper for Definition 2.54: the whole space admits radial segments at every point.

theorem HasFDerivWithinAt.hasGateauxDerivativeWithinAt {H : Type u} {K : Type v} [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup K] [NormedSpace ℝ K] {C : Set H} {T : H → K} {x : H} {A : H →L[ℝ] K} (hT : HasFDerivWithinAt T A C x) (hC : C ∈ nhds x) : HasGateauxDerivativeWithinAt T A C x

A Fréchet derivative within a neighborhood gives the corresponding Gâteaux derivative.

theorem HasFDerivAt.hasGateauxDerivativeAt {H : Type u} {K : Type v} [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup K] [NormedSpace ℝ K] {T : H → K} {x : H} {A : H →L[ℝ] K} (hT : HasFDerivAt T A x) : HasGateauxDerivativeAt T A x

A Fréchet derivative gives the corresponding Gâteaux derivative in the whole space.

theorem hasLineDerivAt_of_hasGateauxDerivativeAt {H : Type u} {K : Type v} [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup K] [NormedSpace ℝ K] {T : H → K} {x : H} {A : H →L[ℝ] K} (hT : HasGateauxDerivativeAt T A x) (y : H) : HasLineDerivAt ℝ T (A y) x y

In the whole space, a Gâteaux derivative yields the corresponding line derivative in every direction.

theorem HasGateauxDerivativeWithinAt.hasLineDerivAt {H : Type u} {K : Type v} [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup K] [NormedSpace ℝ K] {C : Set H} {T : H → K} {x : H} {A : H →L[ℝ] K} (hT : HasGateauxDerivativeWithinAt T A C x) (y : H) : HasLineDerivAt ℝ T (A y) x y

A Gâteaux derivative within C yields the corresponding two-sided line derivative.

theorem hasGateauxDerivativeAt_iff_forall_hasLineDerivAt {H : Type u} {K : Type v} [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup K] [NormedSpace ℝ K] {T : H → K} {x : H} {A : H →L[ℝ] K} : HasGateauxDerivativeAt T A x ↔ ∀ (y : H), HasLineDerivAt ℝ T (A y) x y

Whole-space Gâteaux differentiability is exactly the existence of the corresponding line derivative in every direction.

theorem hasGateauxDerivativeWithinAt_iff_tendsto_directionalDifferenceQuotient {H : Type u} {K : Type v} [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup K] [NormedSpace ℝ K] {C : Set H} {T : H → K} {x : H} {A : H →L[ℝ] K} : HasGateauxDerivativeWithinAt T A C x ↔ HasRadialSegmentsAt C x ∧ ∀ (y : H), Filter.Tendsto (fun (α : ℝ) => (1 / α) • (T (x + α • y) - T x)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (A y))

Definition 2.54 in textbook form: the one-sided line-derivative formulation is equivalent to the convergence of directional difference quotients to A y as the scalar tends to 0 from the right.

theorem HasGateauxDerivativeWithinAt.tendsto_directionalDifferenceQuotient {H : Type u} {K : Type v} [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup K] [NormedSpace ℝ K] {C : Set H} {T : H → K} {x : H} {A : H →L[ℝ] K} (h : HasGateauxDerivativeWithinAt T A C x) (y : H) : Filter.Tendsto (fun (α : ℝ) => (1 / α) • (T (x + α • y) - T x)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (A y))

A Gâteaux derivative provides the textbook directional-difference-quotient limit.

theorem hasGateauxSecondDerivativeWithinAt_iff_tendsto_directionalDifferenceQuotient {H : Type u} {K : Type v} [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup K] [NormedSpace ℝ K] {C : Set H} {T : H → K} {DT : H → H →L[ℝ] K} {x : H} {A₂ : H →L[ℝ] H →L[ℝ] K} : HasGateauxSecondDerivativeWithinAt T DT C x A₂ ↔ HasGateauxDerivativeWithinAt T (DT x) C x ∧ HasRadialSegmentsAt C x ∧ ∀ (y : H), Filter.Tendsto (fun (α : ℝ) => (1 / α) • (DT (x + α • y) - DT x)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (A₂ y))

Definition 2.54 in second-order form: the operator-valued line-derivative formulation for DT is equivalent to the convergence of operator directional difference quotients to A₂ y as the scalar tends to 0 from the right, together with the local first-derivative condition DT x = T'(x).

theorem HasGateauxSecondDerivativeWithinAt.hasGateauxDerivativeWithinAt {H : Type u} {K : Type v} [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup K] [NormedSpace ℝ K] {C : Set H} {T : H → K} {DT : H → H →L[ℝ] K} {x : H} {A₂ : H →L[ℝ] H →L[ℝ] K} (h : HasGateauxSecondDerivativeWithinAt T DT C x A₂) : HasGateauxDerivativeWithinAt T (DT x) C x

A second Gâteaux derivative at x provides the corresponding first Gâteaux derivative there.

theorem HasGateauxSecondDerivativeWithinAt.hasGateauxDerivativeFieldWithinAt {H : Type u} {K : Type v} [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup K] [NormedSpace ℝ K] {C : Set H} {T : H → K} {DT : H → H →L[ℝ] K} {x : H} {A₂ : H →L[ℝ] H →L[ℝ] K} (h : HasGateauxSecondDerivativeWithinAt T DT C x A₂) : HasGateauxDerivativeWithinAt DT A₂ C x

A second Gâteaux derivative at x differentiates the derivative field DT at x.

theorem HasGateauxSecondDerivativeWithinAt.tendsto_directionalDifferenceQuotient {H : Type u} {K : Type v} [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup K] [NormedSpace ℝ K] {C : Set H} {T : H → K} {DT : H → H →L[ℝ] K} {x : H} {A₂ : H →L[ℝ] H →L[ℝ] K} (h : HasGateauxSecondDerivativeWithinAt T DT C x A₂) (y : H) : Filter.Tendsto (fun (α : ℝ) => (1 / α) • (DT (x + α • y) - DT x)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (A₂ y))

A second Gâteaux derivative gives the textbook operator directional-difference-quotient limit for the derivative field DT.

theorem hasGateauxDerivativeAt_iff_tendsto_directionalDifferenceQuotient {H : Type u} {K : Type v} [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup K] [NormedSpace ℝ K] {T : H → K} {x : H} {A : H →L[ℝ] K} : HasGateauxDerivativeAt T A x ↔ ∀ (y : H), Filter.Tendsto (fun (α : ℝ) => (1 / α) • (T (x + α • y) - T x)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (A y))

In the whole space, Definition 2.54 reduces to the directional-difference-quotient limit.

theorem HasGateauxDerivativeAt.tendsto_directionalDifferenceQuotient {H : Type u} {K : Type v} [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup K] [NormedSpace ℝ K] {T : H → K} {x : H} {A : H →L[ℝ] K} (h : HasGateauxDerivativeAt T A x) (y : H) : Filter.Tendsto (fun (α : ℝ) => (1 / α) • (T (x + α • y) - T x)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (A y))

A Gâteaux derivative in the whole space provides the textbook directional-difference-quotient limit.

theorem HasGateauxDerivativeWithinAt.hasRadialSegmentsAt {H : Type u} {K : Type v} [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup K] [NormedSpace ℝ K] {C : Set H} {T : H → K} {x : H} {A : H →L[ℝ] K} (h : HasGateauxDerivativeWithinAt T A C x) : HasRadialSegmentsAt C x

A Gâteaux derivative at x forces the directional segment condition at x.

theorem gateauxDifferentiableWithinAt_iff_exists_hasGateauxDerivativeWithinAt {H : Type u} {K : Type v} [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup K] [NormedSpace ℝ K] {C : Set H} {T : H → K} {x : H} : GateauxDifferentiableWithinAt T C x ↔ ∃ (A : H →L[ℝ] K), HasGateauxDerivativeWithinAt T A C x

T is Gâteaux differentiable within C at x exactly when it admits some Gâteaux derivative there.

theorem gateauxDifferentiableAt_iff_exists_hasGateauxDerivativeAt {H : Type u} {K : Type v} [NormedAddCommGroup H] [NormedSpace ℝ H] [NormedAddCommGroup K] [NormedSpace ℝ K] {T : H → K} {x : H} : GateauxDifferentiableAt T x ↔ ∃ (A : H →L[ℝ] K), HasGateauxDerivativeAt T A x

T is Gâteaux differentiable at x exactly when it admits some Gâteaux derivative there.