English
If f is differentiable near every interior point of s and has a second derivative at x, then f'' v w = f'' w v for any v,w in E, under the appropriate within-at framework.
Русский
Если f дифференцируема вблизи каждого interior точки s и существует вторая производная в x, то f'' v w = f'' w v для любых v,w в E в рамках внутри-на-t.
LaTeX
$$$$ f''(v,w) = f''(w,v). $$$$
Lean4
theorem second_derivative_symmetric_of_eventually [IsRCLikeNormedField 𝕜] {f' : E → E →L[𝕜] F} {x : E}
{f'' : E →L[𝕜] E →L[𝕜] F} (hf : ∀ᶠ y in 𝓝 x, HasFDerivAt f (f' y) y) (hx : HasFDerivAt f' f'' x) (v w : E) :
f'' v w = f'' w v := by
let _ := IsRCLikeNormedField.rclike 𝕜
let _ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
let _ : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
let _ : LinearMap.CompatibleSMul E F ℝ 𝕜 := LinearMap.IsScalarTower.compatibleSMul
let _ : LinearMap.CompatibleSMul E (E →L[𝕜] F) ℝ 𝕜 := LinearMap.IsScalarTower.compatibleSMul
let f'R : E → E →L[ℝ] F := fun x ↦ (f' x).restrictScalars ℝ
have hfR : ∀ᶠ y in 𝓝 x, HasFDerivAt f (f'R y) y := by
filter_upwards [hf] with y hy using HasFDerivAt.restrictScalars ℝ hy
let f''Rl : E →ₗ[ℝ] E →ₗ[ℝ] F :=
{ toFun := fun x ↦
{ toFun := fun y ↦ f'' x y
map_add' := by simp
map_smul' := by simp }
map_add' := by intros; ext; simp
map_smul' := by intros; ext; simp }
let f''R : E →L[ℝ] E →L[ℝ] F :=
by
refine LinearMap.mkContinuous₂ f''Rl (‖f''‖) (fun x y ↦ ?_)
simp only [LinearMap.coe_mk, AddHom.coe_mk, f''Rl]
exact ContinuousLinearMap.le_opNorm₂ f'' x y
have : HasFDerivAt f'R f''R x := by
simp only [hasFDerivAt_iff_tendsto] at hx ⊢
exact hx
change f''R v w = f''R w v
exact second_derivative_symmetric_of_eventually_of_real hfR this v w
