English
There exists a choice n' between minSmoothness 𝕜 m and n such that n' is finite and not equal to ∞, when minSmoothness 𝕜 m ≤ n.
Русский
Существует такое n' между minSmoothness 𝕜 m и n, что n' конечно и не равно ∞, если minSmoothness 𝕜 m ≤ n.
LaTeX
$$$$ \\exists n',\\; \\minSmoothness_{\\mathbb{k}}(m) \\le n' \\le n \\land n' \\neq \\infty. $$$$
Lean4
/-- If a function is `C^2` within a set at a point, and accumulated by points in the interior
of the set, then its second derivative there is symmetric. Over a field
different from `ℝ` or `ℂ`, we should require that the function is analytic. -/
theorem isSymmSndFDerivWithinAt {n : WithTop ℕ∞} (hf : ContDiffWithinAt 𝕜 n f s x) (hn : minSmoothness 𝕜 2 ≤ n)
(hs : UniqueDiffOn 𝕜 s) (hx : x ∈ closure (interior s)) (h'x : x ∈ s) : IsSymmSndFDerivWithinAt 𝕜 f s x := by
/- We argue that, at interior points, the second derivative is symmetric, and moreover by
continuity it converges to the second derivative at `x`. Therefore, the latter is also
symmetric. -/
obtain ⟨m, hm, hmn, m_ne⟩ := exist_minSmoothness_le_ne_infty hn
rcases (hf.of_le hmn).contDiffOn' le_rfl (by simp [m_ne]) with ⟨u, u_open, xu, hu⟩
simp only [insert_eq_of_mem h'x] at hu
have h'u : UniqueDiffOn 𝕜 (s ∩ u) := hs.inter u_open
obtain ⟨y, hy, y_lim⟩ : ∃ y, (∀ (n : ℕ), y n ∈ interior s) ∧ Tendsto y atTop (𝓝 x) := mem_closure_iff_seq_limit.1 hx
have L : ∀ᶠ k in atTop, y k ∈ u := y_lim (u_open.mem_nhds xu)
have I : ∀ᶠ k in atTop, IsSymmSndFDerivWithinAt 𝕜 f s (y k) :=
by
filter_upwards [L] with k hk
have s_mem : s ∈ 𝓝 (y k) := by
apply mem_of_superset (isOpen_interior.mem_nhds (hy k))
exact interior_subset
have : IsSymmSndFDerivAt 𝕜 f (y k) :=
by
apply ContDiffAt.isSymmSndFDerivAt _ (n := m) hm
apply (hu (y k) ⟨(interior_subset (hy k)), hk⟩).contDiffAt
exact inter_mem s_mem (u_open.mem_nhds hk)
intro v w
rw [fderivWithin_fderivWithin_eq_of_mem_nhds s_mem]
exact this v w
have A : ContinuousOn (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s) (s ∩ u) :=
by
have : ContinuousOn (fderivWithin 𝕜 (fderivWithin 𝕜 f (s ∩ u)) (s ∩ u)) (s ∩ u) :=
((hu.fderivWithin h'u (m := 1) (le_minSmoothness.trans hm)).fderivWithin h'u (m := 0) le_rfl).continuousOn
apply this.congr
intro y hy
apply fderivWithin_fderivWithin_eq_of_eventuallyEq
filter_upwards [u_open.mem_nhds hy.2] with z hz
change (z ∈ s) = (z ∈ s ∩ u)
simp_all
have B :
Tendsto (fun k ↦ fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k)) atTop (𝓝 (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x)) :=
by
have : Tendsto y atTop (𝓝[s ∩ u] x) :=
by
apply tendsto_nhdsWithin_iff.2 ⟨y_lim, ?_⟩
filter_upwards [L] with k hk using ⟨interior_subset (hy k), hk⟩
exact (A x ⟨h'x, xu⟩).tendsto.comp this
have C (v w : E) :
Tendsto (fun k ↦ fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k) v w) atTop
(𝓝 (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x v w)) :=
by
have : Continuous (fun (A : E →L[𝕜] E →L[𝕜] F) ↦ A v w) := by fun_prop
exact (this.tendsto _).comp B
have C' (v w : E) :
Tendsto (fun k ↦ fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k) w v) atTop
(𝓝 (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x v w)) :=
by
apply (C v w).congr'
filter_upwards [I] with k hk using hk v w
intro v w
exact tendsto_nhds_unique (C v w) (C' w v)
