nevanlinna/Nevanlinna/partialDeriv.lean

143 lines
4.4 KiB
Plaintext
Raw Normal View History

2024-05-07 09:49:56 +02:00
import Mathlib.Analysis.Calculus.FDeriv.Basic
import Mathlib.Analysis.Calculus.FDeriv.Symmetric
2024-05-09 08:18:55 +02:00
import Mathlib.Analysis.Calculus.ContDiff.Basic
2024-05-07 09:49:56 +02:00
2024-05-07 17:32:41 +02:00
variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
2024-05-08 15:59:56 +02:00
variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
variable {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
2024-05-13 09:48:16 +02:00
variable {G : Type*} [NormedAddCommGroup G] [NormedSpace 𝕜 G]
2024-05-08 15:59:56 +02:00
variable (𝕜)
2024-05-07 09:49:56 +02:00
2024-05-08 15:59:56 +02:00
noncomputable def partialDeriv : E → (E → F) → (E → F) :=
fun v ↦ (fun f ↦ (fun w ↦ fderiv 𝕜 f w v))
2024-05-07 09:49:56 +02:00
2024-05-08 15:59:56 +02:00
theorem partialDeriv_smul₁ {f : E → F} {a : 𝕜} {v : E} : partialDeriv 𝕜 (a • v) f = a • partialDeriv 𝕜 v f := by
unfold partialDeriv
2024-05-07 16:50:57 +02:00
conv =>
left
intro w
rw [map_smul]
2024-05-08 15:59:56 +02:00
theorem partialDeriv_add₁ {f : E → F} {v₁ v₂ : E} : partialDeriv 𝕜 (v₁ + v₂) f = (partialDeriv 𝕜 v₁ f) + (partialDeriv 𝕜 v₂ f) := by
unfold partialDeriv
2024-05-07 16:50:57 +02:00
conv =>
left
intro w
rw [map_add]
2024-05-08 15:59:56 +02:00
theorem partialDeriv_smul₂ {f : E → F} {a : 𝕜} {v : E} (h : Differentiable 𝕜 f) : partialDeriv 𝕜 v (a • f) = a • partialDeriv 𝕜 v f := by
unfold partialDeriv
2024-05-07 09:49:56 +02:00
have : a • f = fun y ↦ a • f y := by rfl
rw [this]
conv =>
left
intro w
rw [fderiv_const_smul (h w)]
2024-05-08 15:59:56 +02:00
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
2024-05-07 12:13:28 +02:00
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)]
2024-05-13 09:48:16 +02:00
theorem partialDeriv_compContLin {f : E → F} {l : F →L[𝕜] G} {v : E} (h : Differentiable 𝕜 f) : partialDeriv 𝕜 v (l ∘ f) = l ∘ partialDeriv 𝕜 v f := by
2024-05-08 15:59:56 +02:00
unfold partialDeriv
2024-05-07 12:13:28 +02:00
conv =>
left
intro w
left
rw [fderiv.comp w (ContinuousLinearMap.differentiableAt l) (h w)]
simp
rfl
2024-05-08 15:59:56 +02:00
theorem partialDeriv_contDiff {n : } {f : E → F} (h : ContDiff 𝕜 (n + 1) f) : ∀ v : E, ContDiff 𝕜 n (partialDeriv 𝕜 v f) := by
unfold partialDeriv
2024-05-07 09:49:56 +02:00
intro v
let A := (contDiff_succ_iff_fderiv.1 h).right
simp at A
2024-05-08 15:59:56 +02:00
have : (fun w => (fderiv 𝕜 f w) v) = (fun f => f v) ∘ (fun w => (fderiv 𝕜 f w)) := by
2024-05-07 09:49:56 +02:00
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
2024-05-07 10:16:23 +02:00
2024-05-08 15:59:56 +02:00
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
2024-05-07 12:13:28 +02:00
2024-05-08 15:59:56 +02:00
unfold partialDeriv
2024-05-07 10:16:23 +02:00
rw [fderiv_clm_apply]
· simp
· exact (contDiff_succ_iff_fderiv.1 hf).2.differentiable le_rfl z
· simp
2024-05-09 10:39:40 +02:00
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
2024-05-08 15:59:56 +02:00
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
2024-05-07 10:16:23 +02:00
intro v₁ v₂
funext z
2024-05-07 12:13:28 +02:00
have derivSymm :
(fderiv (fun w => fderiv f w) z) v₁ v₂ = (fderiv (fun w => fderiv f w) z) v₂ v₁ := by
2024-05-07 10:16:23 +02:00
2024-05-07 12:13:28 +02:00
let f' := fderiv f
have h₀ : ∀ y, HasFDerivAt f (f' y) y := by
intro y
exact DifferentiableAt.hasFDerivAt ((h.differentiable one_le_two) y)
2024-05-07 10:16:23 +02:00
2024-05-07 12:13:28 +02:00
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₂
2024-05-08 15:59:56 +02:00
rw [← partialDeriv_fderiv h z v₂ v₁]
2024-05-07 12:13:28 +02:00
rw [derivSymm]
2024-05-08 15:59:56 +02:00
rw [partialDeriv_fderiv h z v₁ v₂]