18 lines
692 B
Plaintext
18 lines
692 B
Plaintext
|
import Mathlib.Data.Fin.Tuple.Basic
|
|||
|
|
import Mathlib.Analysis.Complex.Basic
|
|||
|
|
import Mathlib.Analysis.Complex.TaylorSeries
|
|||
|
|
import Mathlib.Analysis.Calculus.LineDeriv.Basic
|
|||
|
|
import Mathlib.Analysis.Calculus.ContDiff.Defs
|
|||
|
|
import Mathlib.Analysis.Calculus.FDeriv.Basic
|
|||
|
|
import Mathlib.Analysis.Calculus.FDeriv.Symmetric
|
|||
|
|
|
|||
|
|
|
|||
|
|
lemma l₁ (f : ℝ × ℝ → ℝ) (h : ContDiff ℝ 2 f) :
|
|||
|
|
∀ z a b : ℝ × ℝ, (fderiv ℝ (fun w => fderiv ℝ f w) z) a b = iteratedFDeriv ℝ 2 f z ![a, b] := by
|
|||
|
|
sorry
|
|||
|
|
|
|||
|
|
lemma l₂ (f : ℝ × ℝ → ℝ) (h : ContDiff ℝ 2 f) :
|
|||
|
|
∀ z a b : ℝ × ℝ, (fderiv ℝ (fun w => fderiv ℝ f w) z) a b = (fderiv ℝ (fun w ↦ (fderiv ℝ f w) a) z) b := by
|
|||
|
|
sorry
|
|||
|
|
|