nevanlinna/Nevanlinna/partialDeriv.lean

177 lines
5.5 KiB
Plaintext
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

import Mathlib.Analysis.Calculus.FDeriv.Basic
import Mathlib.Analysis.Calculus.FDeriv.Symmetric
import Mathlib.Analysis.Calculus.ContDiff.Basic
variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
variable {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
variable {G : Type*} [NormedAddCommGroup G] [NormedSpace 𝕜 G]
variable (𝕜)
noncomputable def partialDeriv : E → (E → F) → (E → F) :=
fun v ↦ (fun f ↦ (fun w ↦ fderiv 𝕜 f w v))
theorem partialDeriv_smul₁ {f : E → F} {a : 𝕜} {v : E} : partialDeriv 𝕜 (a • v) f = a • partialDeriv 𝕜 v f := by
unfold partialDeriv
conv =>
left
intro w
rw [map_smul]
theorem partialDeriv_add₁ {f : E → F} {v₁ v₂ : E} : partialDeriv 𝕜 (v₁ + v₂) f = (partialDeriv 𝕜 v₁ f) + (partialDeriv 𝕜 v₂ f) := by
unfold partialDeriv
conv =>
left
intro w
rw [map_add]
theorem partialDeriv_smul₂ {f : E → F} {a : 𝕜} {v : E} (h : Differentiable 𝕜 f) : partialDeriv 𝕜 v (a • f) = a • partialDeriv 𝕜 v f := by
unfold partialDeriv
have : a • f = fun y ↦ a • f y := by rfl
rw [this]
conv =>
left
intro w
rw [fderiv_const_smul (h w)]
theorem partialDeriv_add₂ {f₁ f₂ : E → F} {v : E} (h₁ : Differentiable 𝕜 f₁) (h₂ : Differentiable 𝕜 f₂) : partialDeriv 𝕜 v (f₁ + f₂) = (partialDeriv 𝕜 v f₁) + (partialDeriv 𝕜 v f₂) := by
unfold partialDeriv
have : f₁ + f₂ = fun y ↦ f₁ y + f₂ y := by rfl
rw [this]
conv =>
left
intro w
left
rw [fderiv_add (h₁ w) (h₂ w)]
theorem partialDeriv_compContLin {f : E → F} {l : F →L[𝕜] G} {v : E} (h : Differentiable 𝕜 f) : partialDeriv 𝕜 v (l ∘ f) = l ∘ partialDeriv 𝕜 v f := by
unfold partialDeriv
conv =>
left
intro w
left
rw [fderiv.comp w (ContinuousLinearMap.differentiableAt l) (h w)]
simp
rfl
theorem partialDeriv_compContLinAt {f : E → F} {l : F →L[𝕜] G} {v : E} {x : E} (h : DifferentiableAt 𝕜 f x) : (partialDeriv 𝕜 v (l ∘ f)) x = (l ∘ partialDeriv 𝕜 v f) x:= by
unfold partialDeriv
rw [fderiv.comp x (ContinuousLinearMap.differentiableAt l) h]
simp
theorem partialDeriv_contDiff {n : } {f : E → F} (h : ContDiff 𝕜 (n + 1) f) : ∀ v : E, ContDiff 𝕜 n (partialDeriv 𝕜 v f) := by
unfold partialDeriv
intro v
let A := (contDiff_succ_iff_fderiv.1 h).right
simp at A
have : (fun w => (fderiv 𝕜 f w) v) = (fun f => f v) ∘ (fun w => (fderiv 𝕜 f w)) := by
rfl
rw [this]
refine ContDiff.comp ?hg A
refine ContDiff.of_succ ?hg.h
refine ContDiff.clm_apply ?hg.h.hf ?hg.h.hg
exact contDiff_id
exact contDiff_const
theorem partialDeriv_contDiffAt {n : } {f : E → F} {x : E} (h : ContDiffAt 𝕜 (n + 1) f x) : ∀ v : E, ContDiffAt 𝕜 n (partialDeriv 𝕜 v f) x := by
unfold partialDeriv
intro v
let eval_at_v : (E →L[𝕜] F) →L[𝕜] F :=
{
toFun := fun l ↦ l v
map_add' := by simp
map_smul' := by simp
}
have : (fun w => (fderiv 𝕜 f w) v) = eval_at_v ∘ (fun w => (fderiv 𝕜 f w)) := by
rfl
rw [this]
apply ContDiffAt.continuousLinearMap_comp
-- ContDiffAt 𝕜 (↑n) (fun w => fderiv 𝕜 f w) x
apply ContDiffAt.fderiv_right h
rfl
lemma partialDeriv_fderiv {f : E → F} (hf : ContDiff 𝕜 2 f) (z a b : E) :
fderiv 𝕜 (fderiv 𝕜 f) z b a = partialDeriv 𝕜 b (partialDeriv 𝕜 a f) z := by
unfold partialDeriv
rw [fderiv_clm_apply]
· simp
· exact (contDiff_succ_iff_fderiv.1 hf).2.differentiable le_rfl z
· simp
theorem partialDeriv_eventuallyEq {f₁ f₂ : E → F} {x : E} (h : f₁ =ᶠ[nhds x] f₂) : ∀ v : E, partialDeriv 𝕜 v f₁ x = partialDeriv 𝕜 v f₂ x := by
unfold partialDeriv
rw [Filter.EventuallyEq.fderiv_eq h]
exact fun v => rfl
section restrictScalars
variable (𝕜 : Type*) [NontriviallyNormedField 𝕜]
variable {𝕜' : Type*} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜']
variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E]
variable [IsScalarTower 𝕜 𝕜' E]
variable {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace 𝕜' F]
variable [IsScalarTower 𝕜 𝕜' F]
--variable {f : E → F}
theorem partialDeriv_restrictScalars {f : E → F} {v : E} :
Differentiable 𝕜' f → partialDeriv 𝕜 v f = partialDeriv 𝕜' v f := by
intro hf
unfold partialDeriv
funext x
rw [(hf x).fderiv_restrictScalars 𝕜]
simp
theorem partialDeriv_comm
{E : Type*} [NormedAddCommGroup E] [NormedSpace E]
{F : Type*} [NormedAddCommGroup F] [NormedSpace F]
{f : E → F} (h : ContDiff 2 f) :
∀ v₁ v₂ : E, partialDeriv v₁ (partialDeriv v₂ f) = partialDeriv v₂ (partialDeriv v₁ f) := by
intro v₁ v₂
funext z
have derivSymm :
(fderiv (fun w => fderiv f w) z) v₁ v₂ = (fderiv (fun w => fderiv f w) z) v₂ v₁ := by
let f' := fderiv f
have h₀ : ∀ y, HasFDerivAt f (f' y) y := by
intro y
exact DifferentiableAt.hasFDerivAt ((h.differentiable one_le_two) y)
let f'' := (fderiv f' z)
have h₁ : HasFDerivAt f' f'' z := by
apply DifferentiableAt.hasFDerivAt
apply (contDiff_succ_iff_fderiv.1 h).right.differentiable (Submonoid.oneLE.proof_2 ℕ∞)
apply second_derivative_symmetric h₀ h₁ v₁ v₂
rw [← partialDeriv_fderiv h z v₂ v₁]
rw [derivSymm]
rw [partialDeriv_fderiv h z v₁ v₂]