Michal–Bastiani calculus on locally convex spaces

Reference: K.-H. Neeb, Towards a Lie theory of locally convex groups, Jpn. J. Math. 1 (2006), 291–468 (arXiv:1501.06269), §I.2; H. Glöckner, K.-H. Neeb, Infinite-Dimensional Lie Groups (arXiv:2602.12362), Ch. 2.

For E, F real topological vector spaces, U ⊆ E open and f : E → F:

• dMB f (x, h) = d/dt|_{t=0} f (x + t • h) is the directional derivative (Definition I.2.1).
• f is C^1 on U if all directional derivatives exist on U and dMB f : E × E → F is continuous on U × E.
• f is C^{k+1} on U if it is C^1 and dMB f is C^k on U × E. This recursive definition is equivalent to Neeb's (continuity of all the iterated derivatives d^j f, see contDiffMBOn_iff_hasContIterDerivOn in LCAnalysis.Higher); it is the one used by Glöckner, and it avoids j-linear maps.

The directional derivative is defined literally as the limit of difference quotients, so no normed structure is involved anywhere (Mathlib's HasDerivAt makes sense for curves in a topological vector space, but its API is mostly stated for normed targets). To use the one-variable calculus of Mathlib we compose with continuous linear functionals F →L[ℝ] ℝ. Local convexity (and T2) only appear in the theorems: through Hahn–Banach, functionals separate points, which is what makes the fundamental theorem of calculus, hence the chain rule, work (Neeb, Example I.2.5).

Directional derivatives and C^k maps (Definition I.2.1)

def LCAnalysis.HasDirDerivAt {E : Type u} [AddCommGroup E] [Module ℝ E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] (f : E → F) (x h : E) (y : F) : Prop

f has derivative y at x in the direction h: t⁻¹ • (f (x + t • h) - f x) → y as t → 0, t ≠ 0.

Equations

• LCAnalysis.HasDirDerivAt f x h y = Filter.Tendsto (fun (t : ℝ) => t⁻¹ • (f (x + t • h) - f x)) (nhdsWithin 0 {0}ᶜ) (nhds y)

noncomputable def LCAnalysis.dMB {E : Type u} [AddCommGroup E] [Module ℝ E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] (f : E → F) (p : E × E) : F

The directional derivative df(x)(h), as a function on E × E (junk value where it does not exist).

Equations

• LCAnalysis.dMB f p = (nhdsWithin 0 {0}ᶜ).limUnder fun (t : ℝ) => t⁻¹ • (f (p.1 + t • p.2) - f p.1)

def LCAnalysis.ContDiffMBOn {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] : ℕ → {E : Type u} → [inst : AddCommGroup E] → [Module ℝ E] → [TopologicalSpace E] → (E → F) → Set E → Prop

C^k maps in the sense of Michal–Bastiani on a set U (meant to be open), k ∈ ℕ.

Equations

• One or more equations did not get rendered due to their size.
• LCAnalysis.ContDiffMBOn 0 x✝¹ x✝ = ContinuousOn x✝¹ x✝

def LCAnalysis.SmoothMBOn {E : Type u} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] (f : E → F) (U : Set E) : Prop

Smooth maps in the sense of Michal–Bastiani.

Equations

• LCAnalysis.SmoothMBOn f U = ∀ (k : ℕ), LCAnalysis.ContDiffMBOn k f U

Basic properties

theorem LCAnalysis.ContDiffMBOn.continuousOn {E : Type u} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {k : ℕ} {f : E → F} {U : Set E} (hf : ContDiffMBOn k f U) : ContinuousOn f U

theorem LCAnalysis.ContDiffMBOn.hasDirDerivAt {E : Type u} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {k : ℕ} {f : E → F} {U : Set E} (hf : ContDiffMBOn (k + 1) f U) {x : E} (hx : x ∈ U) (h : E) : HasDirDerivAt f x h (dMB f (x, h))

theorem LCAnalysis.ContDiffMBOn.of_succ {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {k : ℕ} {E : Type u} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {f : E → F} {U : Set E} : ContDiffMBOn (k + 1) f U → ContDiffMBOn k f U

theorem LCAnalysis.ContDiffMBOn.of_le {E : Type u} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {k l : ℕ} {f : E → F} {U : Set E} (hf : ContDiffMBOn k f U) (hlk : l ≤ k) : ContDiffMBOn l f U

theorem LCAnalysis.SmoothMBOn.contDiffMBOn {E : Type u} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {f : E → F} {U : Set E} (hf : SmoothMBOn f U) (k : ℕ) : ContDiffMBOn k f U

Proposition I.2.3

theorem LCAnalysis.HasDirDerivAt.hasDerivAt_clm {E : Type u} [AddCommGroup E] [Module ℝ E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {f : E → F} {x h : E} {t : ℝ} {y : F} (hd : HasDirDerivAt f (x + t • h) h y) (φ : F →L[ℝ] ℝ) : HasDerivAt (fun (s : ℝ) => φ (f (x + s • h))) (φ y) t

Along the line t ↦ x + t • h, a directional derivative composed with a continuous linear functional is an ordinary derivative.

theorem LCAnalysis.HasDirDerivAt.dMB_eq {E : Type u} [AddCommGroup E] [Module ℝ E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [T2Space F] {f : E → F} {x h : E} {y : F} (hd : HasDirDerivAt f x h y) : dMB f (x, h) = y

theorem LCAnalysis.HasDirDerivAt.smul_dir {E : Type u} [AddCommGroup E] [Module ℝ E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [ContinuousSMul ℝ F] [T2Space F] {f : E → F} {x h : E} {y : F} (hd : HasDirDerivAt f x h y) (c : ℝ) : HasDirDerivAt f x (c • h) (c • y)

Homogeneity of directional derivatives in the direction.

theorem LCAnalysis.ContDiffMBOn.dMB_smul {E : Type u} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [ContinuousSMul ℝ F] [T2Space F] {f : E → F} {U : Set E} (hf : ContDiffMBOn 1 f U) {x : E} (hx : x ∈ U) (c : ℝ) (h : E) : dMB f (x, c • h) = c • dMB f (x, h)

theorem LCAnalysis.ContDiffMBOn.continuous_dMB {E : Type u} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {f : E → F} {U : Set E} (hf : ContDiffMBOn 1 f U) {x : E} (hx : x ∈ U) : Continuous fun (h : E) => dMB f (x, h)

h ↦ df(x)(h) is continuous.

theorem LCAnalysis.ContDiffMBOn.dMB_add {E : Type u} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [ContinuousSMul ℝ F] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [IsTopologicalAddGroup F] [LocallyConvexSpace ℝ F] [T2Space F] {f : E → F} {U : Set E} (hU : IsOpen U) (hf : ContDiffMBOn 1 f U) {x : E} (hx : x ∈ U) (h k : E) : dMB f (x, h + k) = dMB f (x, h) + dMB f (x, k)

Additivity of df(x). The proof applies the mean value theorem to φ ∘ f along lines, for continuous linear functionals φ, and uses that these separate points (Hahn–Banach).

theorem LCAnalysis.ContDiffMBOn.exists_clm {E : Type u} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [ContinuousSMul ℝ F] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [IsTopologicalAddGroup F] [LocallyConvexSpace ℝ F] [T2Space F] {f : E → F} {U : Set E} (hU : IsOpen U) (hf : ContDiffMBOn 1 f U) {x : E} (hx : x ∈ U) : ∃ (L : E →L[ℝ] F), ∀ (h : E), L h = dMB f (x, h)

(i) For a C^1 map, df(x) is a continuous linear map.

theorem LCAnalysis.ContDiffMBOn.integral_dMB {E : Type u} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] {f : E → F} {U : Set E} (hf : ContDiffMBOn 1 f U) {x h : E} (hxh : ∀ t ∈ Set.Icc 0 1, x + t • h ∈ U) (φ : F →L[ℝ] ℝ) : φ (f (x + h)) - φ (f x) = ∫ (t : ℝ) in 0..1, φ (dMB f (x + t • h, h))

(ii) Fundamental theorem of calculus, in weak form (no completeness assumption on F): for every continuous linear functional φ, φ (f (x + h)) - φ (f x) = ∫₀¹ φ (df(x + t h)(h)) dt.

The chain rule

The key step (Glöckner's characterization of C^1): the difference quotient t⁻¹ • (g (y + t • v) - g y) extends continuously to t = 0 by dg(y)(v). The proof combines the weak fundamental theorem of calculus with Hahn–Banach (the quotient lies in the closed convex hull of {dg(y + s t v)(v) : s ∈ [0, 1]}) and local convexity (closed convex neighborhoods form a basis).

theorem LCAnalysis.ContDiffMBOn.quotient_mem_closure_convexHull {E : Type u} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [ContinuousSMul ℝ F] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [IsTopologicalAddGroup F] [LocallyConvexSpace ℝ F] [T2Space F] {g : E → F} {U : Set E} (hg : ContDiffMBOn 1 g U) {y v : E} {t : ℝ} (ht : t ≠ 0) (hseg : ∀ s ∈ Set.Icc 0 1, y + s • t • v ∈ U) : t⁻¹ • (g (y + t • v) - g y) ∈ closure ((convexHull ℝ) ((fun (s : ℝ) => dMB g (y + s • t • v, v)) '' Set.Icc 0 1))

Mean value inclusion: the difference quotient lies in the closed convex hull of the directional derivatives along the segment.

theorem LCAnalysis.ContDiffMBOn.tendsto_quotient {E : Type u} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [ContinuousSMul ℝ F] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [IsTopologicalAddGroup F] [LocallyConvexSpace ℝ F] [T2Space F] {g : E → F} {U : Set E} (hU : IsOpen U) (hg : ContDiffMBOn 1 g U) {y v : E} (hy : y ∈ U) : Filter.Tendsto (fun (p : E × E × ℝ) => p.2.2⁻¹ • (g (p.1 + p.2.2 • p.2.1) - g p.1)) (nhdsWithin (y, v, 0) {p : E × E × ℝ | p.2.2 ≠ 0}) (nhds (dMB g (y, v)))

Glöckner's lemma: for g of class C^1, the difference quotient t⁻¹ • (g (y + t • v) - g y) tends to dg(y)(v) as (y', v', t) → (y, v, 0) with t ≠ 0.

theorem LCAnalysis.ContDiffMBOn.hasDirDerivAt_comp {E : Type u} [AddCommGroup E] [Module ℝ E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [ContinuousSMul ℝ F] [IsTopologicalAddGroup F] {G : Type u_1} [AddCommGroup G] [Module ℝ G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousSMul ℝ G] [LocallyConvexSpace ℝ G] [T2Space G] {f : E → F} {g : F → G} {V : Set F} (hV : IsOpen V) (hg : ContDiffMBOn 1 g V) {x h : E} {y : F} (hf : HasDirDerivAt f x h y) (hfx : f x ∈ V) : HasDirDerivAt (g ∘ f) x h (dMB g (f x, y))

Chain rule for directional derivatives.

theorem LCAnalysis.ContDiffMBOn.comp_one {E : Type u} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [ContinuousSMul ℝ F] [IsTopologicalAddGroup F] {G : Type u_1} [AddCommGroup G] [Module ℝ G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousSMul ℝ G] [LocallyConvexSpace ℝ G] [T2Space G] {f : E → F} {g : F → G} {U : Set E} {V : Set F} (hV : IsOpen V) (hg : ContDiffMBOn 1 g V) (hf : ContDiffMBOn 1 f U) (hUV : Set.MapsTo f U V) : ContDiffMBOn 1 (g ∘ f) U ∧ ∀ x ∈ U, ∀ (h : E), dMB (g ∘ f) (x, h) = dMB g (f x, dMB f (x, h))

Chain rule for C^1 maps, with the formula d(g ∘ f)(x) = dg(f x) ∘ df(x).

Rules for C^k maps

theorem LCAnalysis.HasDirDerivAt.congr_of_eventuallyEq {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {E₁ : Type u_2} [AddCommGroup E₁] [Module ℝ E₁] [TopologicalSpace E₁] [IsTopologicalAddGroup E₁] [ContinuousSMul ℝ E₁] {f₁ f₂ : E₁ → F} {x h : E₁} {y : F} (hd : HasDirDerivAt f₁ x h y) (heq : f₁ =ᶠ[nhds x] f₂) : HasDirDerivAt f₂ x h y

theorem LCAnalysis.ContDiffMBOn.congr_of_isOpen {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [T2Space F] {k : ℕ} {E₁ : Type u} [AddCommGroup E₁] [Module ℝ E₁] [TopologicalSpace E₁] [IsTopologicalAddGroup E₁] [ContinuousSMul ℝ E₁] [LocallyConvexSpace ℝ E₁] [T2Space E₁] {f₁ f₂ : E₁ → F} {U : Set E₁} : IsOpen U → Set.EqOn f₁ f₂ U → ContDiffMBOn k f₁ U → ContDiffMBOn k f₂ U

C^k only depends on the values on the open set.

theorem LCAnalysis.HasDirDerivAt.prodMk {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {G : Type u_1} [AddCommGroup G] [Module ℝ G] [TopologicalSpace G] {E₁ : Type u_2} [AddCommGroup E₁] [Module ℝ E₁] {f : E₁ → F} {g : E₁ → G} {x h : E₁} {y : F} {z : G} (hf : HasDirDerivAt f x h y) (hg : HasDirDerivAt g x h z) : HasDirDerivAt (fun (w : E₁) => (f w, g w)) x h (y, z)

theorem LCAnalysis.ContDiffMBOn.prodMk {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [T2Space F] {G : Type u_1} [AddCommGroup G] [Module ℝ G] [TopologicalSpace G] [T2Space G] {k : ℕ} {E₁ : Type u} [AddCommGroup E₁] [Module ℝ E₁] [TopologicalSpace E₁] [IsTopologicalAddGroup E₁] [ContinuousSMul ℝ E₁] [LocallyConvexSpace ℝ E₁] [T2Space E₁] {f : E₁ → F} {g : E₁ → G} {U : Set E₁} : IsOpen U → ContDiffMBOn k f U → ContDiffMBOn k g U → ContDiffMBOn k (fun (w : E₁) => (f w, g w)) U

Pairs of C^k maps are C^k.

theorem LCAnalysis.ContDiffMBOn.comp_clm {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [T2Space F] {k : ℕ} {E₁ : Type u} [AddCommGroup E₁] [Module ℝ E₁] [TopologicalSpace E₁] [IsTopologicalAddGroup E₁] [ContinuousSMul ℝ E₁] [LocallyConvexSpace ℝ E₁] [T2Space E₁] {E₂ : Type u_2} [AddCommGroup E₂] [Module ℝ E₂] [TopologicalSpace E₂] [IsTopologicalAddGroup E₂] [ContinuousSMul ℝ E₂] [LocallyConvexSpace ℝ E₂] [T2Space E₂] (L : E₁ →L[ℝ] E₂) {f : E₂ → F} {U : Set E₂} : IsOpen U → ContDiffMBOn k f U → ContDiffMBOn k (f ∘ ⇑L) (⇑L ⁻¹' U)

Precomposition with a continuous linear map preserves C^k.

theorem ContinuousLinearMap.hasDirDerivAt {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {E₁ : Type u_2} [AddCommGroup E₁] [Module ℝ E₁] [TopologicalSpace E₁] (L : E₁ →L[ℝ] F) (x h : E₁) : LCAnalysis.HasDirDerivAt (⇑L) x h (L h)

theorem ContinuousLinearMap.contDiffMBOn {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [T2Space F] (k : ℕ) {E₁ : Type u} [AddCommGroup E₁] [Module ℝ E₁] [TopologicalSpace E₁] [IsTopologicalAddGroup E₁] [ContinuousSMul ℝ E₁] [LocallyConvexSpace ℝ E₁] [T2Space E₁] (L : E₁ →L[ℝ] F) (U : Set E₁) : LCAnalysis.ContDiffMBOn k (⇑L) U

Remark I.2.4: continuous linear maps are C^k for every k.

theorem ContinuousLinearMap.smoothMBOn {E : Type u} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] [T2Space E] [T2Space F] (L : E →L[ℝ] F) (U : Set E) : LCAnalysis.SmoothMBOn (⇑L) U

Remark I.2.4: continuous linear maps are smooth.

theorem LCAnalysis.smoothMBOn_id {E : Type u} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] [T2Space E] (U : Set E) : SmoothMBOn id U

theorem LCAnalysis.ContDiffMBOn.comp {G : Type u_1} [AddCommGroup G] [Module ℝ G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousSMul ℝ G] [LocallyConvexSpace ℝ G] [T2Space G] {k : ℕ} {E₁ : Type u} [AddCommGroup E₁] [Module ℝ E₁] [TopologicalSpace E₁] [IsTopologicalAddGroup E₁] [ContinuousSMul ℝ E₁] [LocallyConvexSpace ℝ E₁] [T2Space E₁] {F₁ : Type v} [AddCommGroup F₁] [Module ℝ F₁] [TopologicalSpace F₁] [IsTopologicalAddGroup F₁] [ContinuousSMul ℝ F₁] [LocallyConvexSpace ℝ F₁] [T2Space F₁] {f : E₁ → F₁} {g : F₁ → G} {U : Set E₁} {V : Set F₁} : IsOpen U → IsOpen V → ContDiffMBOn k g V → ContDiffMBOn k f U → Set.MapsTo f U V → ContDiffMBOn k (g ∘ f) U

(vi) Chain rule for C^k maps.

theorem LCAnalysis.ContDiffMBOn.mono {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {k : ℕ} {E₁ : Type u} [AddCommGroup E₁] [Module ℝ E₁] [TopologicalSpace E₁] [IsTopologicalAddGroup E₁] [ContinuousSMul ℝ E₁] [LocallyConvexSpace ℝ E₁] [T2Space E₁] {f : E₁ → F} {U V : Set E₁} : ContDiffMBOn k f U → V ⊆ U → ContDiffMBOn k f V

theorem LCAnalysis.ContDiffMBOn.of_local {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {k : ℕ} {E₁ : Type u} [AddCommGroup E₁] [Module ℝ E₁] [TopologicalSpace E₁] [IsTopologicalAddGroup E₁] [ContinuousSMul ℝ E₁] [LocallyConvexSpace ℝ E₁] [T2Space E₁] {f : E₁ → F} {U : Set E₁} : IsOpen U → (∀ x ∈ U, ∃ (W : Set E₁), IsOpen W ∧ x ∈ W ∧ ContDiffMBOn k f (U ∩ W)) → ContDiffMBOn k f U

Being C^k is a local property.

theorem LCAnalysis.ContDiffMBOn.dMB_comp {E : Type u} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [ContinuousSMul ℝ F] [IsTopologicalAddGroup F] {G : Type u_1} [AddCommGroup G] [Module ℝ G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousSMul ℝ G] [LocallyConvexSpace ℝ G] [T2Space G] {f : E → F} {g : F → G} {U : Set E} {V : Set F} (hV : IsOpen V) (hg : ContDiffMBOn 1 g V) (hf : ContDiffMBOn 1 f U) (hUV : Set.MapsTo f U V) {x : E} (hx : x ∈ U) (h : E) : dMB (g ∘ f) (x, h) = dMB g (f x, dMB f (x, h))

(vi) Chain rule: formula for the derivative.

Mean value inclusion and partial derivatives (Michor 1980, 8.3–8.4)

theorem LCAnalysis.exists_closed_convex_nhds_subset {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [ContinuousSMul ℝ F] [IsTopologicalAddGroup F] [LocallyConvexSpace ℝ F] {a : F} {N : Set F} (hN : N ∈ nhds a) : ∃ W ∈ nhds a, IsClosed W ∧ Convex ℝ W ∧ W ⊆ N

Closed convex neighborhoods form a basis in a locally convex space.

theorem LCAnalysis.integral_of_hasDirDerivAt {E : Type u} [AddCommGroup E] [Module ℝ E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {f : E → F} {z w : E} {D : ℝ → F} (hd : ∀ s ∈ Set.Icc 0 1, HasDirDerivAt f (z + s • w) w (D s)) (hD : ContinuousOn D (Set.Icc 0 1)) (φ : F →L[ℝ] ℝ) : φ (f (z + w)) - φ (f z) = ∫ (s : ℝ) in 0..1, φ (D s)

Weak fundamental theorem of calculus along a segment, assuming only the directional derivatives in the direction of the segment.

theorem LCAnalysis.sub_mem_of_hasDirDerivAt {E : Type u} [AddCommGroup E] [Module ℝ E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [ContinuousSMul ℝ F] [IsTopologicalAddGroup F] [LocallyConvexSpace ℝ F] {f : E → F} {z w : E} {D : ℝ → F} (hd : ∀ s ∈ Set.Icc 0 1, HasDirDerivAt f (z + s • w) w (D s)) (hD : ContinuousOn D (Set.Icc 0 1)) {W : Set F} (hWc : Convex ℝ W) (hWcl : IsClosed W) (hDW : ∀ s ∈ Set.Icc 0 1, D s ∈ W) : f (z + w) - f z ∈ W

Mean value inclusion (Michor 8.4, remark): the increment along a segment lies in every closed convex set containing the directional derivatives along the segment.

theorem LCAnalysis.tendsto_quotient_of_hasDirDerivAt {E : Type u} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [ContinuousSMul ℝ F] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [IsTopologicalAddGroup F] [LocallyConvexSpace ℝ F] [T2Space F] {f : E → F} {U : Set E} (hU : IsOpen U) {w : E} {D : E → F} (hd : ∀ q ∈ U, HasDirDerivAt f q w (D q)) (hD : ContinuousOn D U) {p : E} (hp : p ∈ U) : Filter.Tendsto (fun (r : E × ℝ) => r.2⁻¹ • (f (r.1 + r.2 • w) - f r.1)) (nhdsWithin (p, 0) {r : E × ℝ | r.2 ≠ 0}) (nhds (D p))

Directional difference quotients converge locally uniformly in the base point: if f has directional derivative D q in the direction w at every q ∈ U, with D continuous, then t⁻¹ • (f (q + t • w) - f q) → D p as (q, t) → (p, 0), t ≠ 0.

theorem LCAnalysis.continuousOn_of_hasDirDerivAt {E : Type u} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [ContinuousSMul ℝ F] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [IsTopologicalAddGroup F] [LocallyConvexSpace ℝ F] [T2Space F] {f : E → F} {U : Set E} (hU : IsOpen U) {D : E × E → F} (hd : ∀ q ∈ U, ∀ (w : E), HasDirDerivAt f q w (D (q, w))) (hD : ContinuousOn D (U ×ˢ Set.univ)) : ContinuousOn f U

A map with jointly continuous directional derivatives is continuous (Michor 8.1).

theorem LCAnalysis.contDiffMBOn_one_of_partials {E : Type u} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [ContinuousSMul ℝ F] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [IsTopologicalAddGroup F] {G : Type u_1} [AddCommGroup G] [Module ℝ G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousSMul ℝ G] [LocallyConvexSpace ℝ G] [T2Space G] {f : E × F → G} {U : Set (E × F)} (hU : IsOpen U) {d₁ : E × F → E → G} {d₂ : E × F → F → G} (h₁ : ∀ p ∈ U, ∀ (u : E), HasDirDerivAt f p (u, 0) (d₁ p u)) (h₂ : ∀ p ∈ U, ∀ (v : F), HasDirDerivAt f p (0, v) (d₂ p v)) (hc₁ : ContinuousOn (fun (q : (E × F) × E) => d₁ q.1 q.2) (U ×ˢ Set.univ)) (hc₂ : ContinuousOn (fun (q : (E × F) × F) => d₂ q.1 q.2) (U ×ˢ Set.univ)) : ContDiffMBOn 1 f U ∧ ∀ p ∈ U, ∀ (u : E) (v : F), dMB f (p, u, v) = d₁ p u + d₂ p v

Michor 1980, Lemma 8.3: a map on an open subset of E × F whose partial directional derivatives exist and are jointly continuous is C^1, with df(p)(u, v) = D₁f(p) u + D₂f(p) v.

Proposition I.2.3 (ii) second part, and (iv)

theorem LCAnalysis.ContDiffMBOn.eqOn_of_dMB_eq_zero {E : Type u} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [ContinuousSMul ℝ F] [LocallyConvexSpace ℝ E] [IsTopologicalAddGroup F] [LocallyConvexSpace ℝ F] [T2Space F] {f : E → F} {U : Set E} (hU : IsOpen U) (hUc : IsPreconnected U) (hf : ContDiffMBOn 1 f U) (h0 : ∀ x ∈ U, ∀ (h : E), dMB f (x, h) = 0) {x y : E} (hx : x ∈ U) (hy : y ∈ U) : f x = f y

(ii) A C^1 map on a connected open set with df = 0 is constant.

theorem LCAnalysis.HasDirDerivAt.sub {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [IsTopologicalAddGroup F] {E₁ : Type u_2} [AddCommGroup E₁] [Module ℝ E₁] {f g : E₁ → F} {x h : E₁} {a b : F} (hf : HasDirDerivAt f x h a) (hg : HasDirDerivAt g x h b) : HasDirDerivAt (fun (y : E₁) => f y - g y) x h (a - b)

theorem LCAnalysis.HasDirDerivAt.comp_add_const {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {E₁ : Type u_2} [AddCommGroup E₁] [Module ℝ E₁] {f : E₁ → F} {y c w : E₁} {a : F} (hf : HasDirDerivAt f (y + c) w a) : HasDirDerivAt (fun (z : E₁) => f (z + c)) y w a

theorem LCAnalysis.ContDiffMBOn.second_diff_mem {E : Type u} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [ContinuousSMul ℝ F] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [IsTopologicalAddGroup F] [LocallyConvexSpace ℝ F] [T2Space F] {f : E → F} {U : Set E} (hU : IsOpen U) (hf : ContDiffMBOn 2 f U) {x : E} (hx : x ∈ U) (h₁ h₂ : E) {W : Set F} (hW : W ∈ nhds (dMB (dMB f) ((x, h₁), h₂, 0))) (hWcl : IsClosed W) (hWc : Convex ℝ W) : ∀ᶠ (t : ℝ) in nhdsWithin 0 {0}ᶜ, (t * t)⁻¹ • (f (x + t • h₁ + t • h₂) - f (x + t • h₁) - f (x + t • h₂) + f x) ∈ W

The key estimate for the symmetry of the second derivative: the second difference f (x + t h₁ + t h₂) - f (x + t h₁) - f (x + t h₂) + f x, divided by t², eventually lies in any closed convex neighborhood of d²f(x)(h₁, h₂). Two applications of the mean value inclusion.

theorem LCAnalysis.ContDiffMBOn.dMB_dMB_symm {E : Type u} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {F : Type v} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [ContinuousSMul ℝ F] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [IsTopologicalAddGroup F] [LocallyConvexSpace ℝ F] [T2Space F] {f : E → F} {U : Set E} (hU : IsOpen U) (hf : ContDiffMBOn 2 f U) {x : E} (hx : x ∈ U) (h₁ h₂ : E) : dMB (dMB f) ((x, h₁), h₂, 0) = dMB (dMB f) ((x, h₂), h₁, 0)

(iv) Symmetry of the second derivative.