English
Let f be differentiable inside a convex set s with nonempty interior. If f' and f'' exist inside interior s at x, then f'' v w = f'' w v for all v,w in E.
Русский
Пусть f дифференцируема внутри выпуклого s с непустымInterior. Если существуют f', f'' внутри interior s в x, то f'' v w = f'' w v для всех v,w в E.
LaTeX
$$$$ f''(v,w) = f''(w,v). $$$$
Lean4
/-- If a function is differentiable inside a convex set with nonempty interior, and has a second
derivative at a point of this convex set, then this second derivative is symmetric. -/
theorem second_derivative_within_at_symmetric {s : Set E} (s_conv : Convex ℝ s) (hne : (interior s).Nonempty)
{f : E → F} {f' : E → E →L[ℝ] F} {f'' : E →L[ℝ] E →L[ℝ] F} (hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x) {x : E}
(xs : x ∈ s) (hx : HasFDerivWithinAt f' f'' (interior s) x) (v w : E) : f'' v w = f'' w v := by
/- we work around a point `x + 4 z` in the interior of `s`. For any vector `m`,
then `x + 4 (z + t m)` also belongs to the interior of `s` for small enough `t`. This means that
we will be able to apply `second_derivative_within_at_symmetric_of_mem_interior` to show
that `f''` is symmetric, after cancelling all the contributions due to `z`. -/
rcases hne with ⟨y, hy⟩
obtain ⟨z, hz⟩ : ∃ z, z = ((1 : ℝ) / 4) • (y - x) := ⟨((1 : ℝ) / 4) • (y - x), rfl⟩
have A : ∀ m : E, Filter.Tendsto (fun t : ℝ => x + (4 : ℝ) • (z + t • m)) (𝓝 0) (𝓝 y) :=
by
intro m
have : x + (4 : ℝ) • (z + (0 : ℝ) • m) = y := by simp [hz]
rw [← this]
refine tendsto_const_nhds.add <| tendsto_const_nhds.smul <| tendsto_const_nhds.add ?_
exact continuousAt_id.smul continuousAt_const
have B : ∀ m : E, ∀ᶠ t in 𝓝[>] (0 : ℝ), x + (4 : ℝ) • (z + t • m) ∈ interior s :=
by
intro m
apply nhdsWithin_le_nhds
apply A m
rw [mem_interior_iff_mem_nhds] at hy
exact interior_mem_nhds.2 hy
choose t ts tpos using fun m => ((B m).and self_mem_nhdsWithin).exists
have C : ∀ m : E, f'' m z = f'' z m := by
intro m
have : f'' (z + t m • m) (z + t 0 • (0 : E)) = f'' (z + t 0 • (0 : E)) (z + t m • m) :=
s_conv.second_derivative_within_at_symmetric_of_mem_interior hf xs hx (ts 0) (ts m)
simp only [ContinuousLinearMap.map_add, ContinuousLinearMap.map_smul, add_right_inj, ContinuousLinearMap.add_apply,
Pi.smul_apply, ContinuousLinearMap.coe_smul', add_zero, smul_zero] at this
exact smul_right_injective F (tpos m).ne' this
have : f'' (z + t v • v) (z + t w • w) = f'' (z + t w • w) (z + t v • v) :=
s_conv.second_derivative_within_at_symmetric_of_mem_interior hf xs hx (ts w) (ts v)
simp only [ContinuousLinearMap.map_add, ContinuousLinearMap.map_smul, smul_smul, ContinuousLinearMap.add_apply,
Pi.smul_apply, ContinuousLinearMap.coe_smul', C] at this
have : (t v * t w) • (f'' v) w = (t v * t w) • (f'' w) v := by linear_combination (norm := module) this
apply smul_right_injective F _ this
simp [(tpos v).ne', (tpos w).ne']
