This commit is contained in:
Stefan Kebekus 2024-06-04 12:30:25 +02:00
parent 6eea56e788
commit 80486cc56c
2 changed files with 86 additions and 0 deletions

View File

@ -131,6 +131,77 @@ theorem laplace_add_ContDiffOn
rw [add_comm] rw [add_comm]
theorem laplace_add_ContDiffAt
{f₁ f₂ : → F}
{x : }
(h₁ : ContDiffAt 2 f₁ x)
(h₂ : ContDiffAt 2 f₂ x) :
Δ (f₁ + f₂) x = (Δ f₁) x + (Δ f₂) x := by
unfold Complex.laplace
simp
have hf₁ : ∀ z ∈ s, DifferentiableAt f₁ z := by
intro z hz
convert DifferentiableOn.differentiableAt _ (IsOpen.mem_nhds hs hz)
apply ContDiffOn.differentiableOn h₁ one_le_two
have hf₂ : ∀ z ∈ s, DifferentiableAt f₂ z := by
intro z hz
convert DifferentiableOn.differentiableAt _ (IsOpen.mem_nhds hs hz)
apply ContDiffOn.differentiableOn h₂ one_le_two
have : partialDeriv 1 (f₁ + f₂) =ᶠ[nhds x] (partialDeriv 1 f₁) + (partialDeriv 1 f₂) := by
apply Filter.eventuallyEq_iff_exists_mem.2
use s
constructor
· exact IsOpen.mem_nhds hs hx
· intro z hz
apply partialDeriv_add₂_differentiableAt
exact hf₁ z hz
exact hf₂ z hz
rw [partialDeriv_eventuallyEq this]
have t₁ : DifferentiableAt (partialDeriv 1 f₁) x := by
let B₀ := (h₁ x hx).contDiffAt (IsOpen.mem_nhds hs hx)
let A₀ := partialDeriv_contDiffAt B₀ 1
exact A₀.differentiableAt (Submonoid.oneLE.proof_2 ℕ∞)
have t₂ : DifferentiableAt (partialDeriv 1 f₂) x := by
let B₀ := (h₂ x hx).contDiffAt (IsOpen.mem_nhds hs hx)
let A₀ := partialDeriv_contDiffAt B₀ 1
exact A₀.differentiableAt (Submonoid.oneLE.proof_2 ℕ∞)
rw [partialDeriv_add₂_differentiableAt t₁ t₂]
have : partialDeriv Complex.I (f₁ + f₂) =ᶠ[nhds x] (partialDeriv Complex.I f₁) + (partialDeriv Complex.I f₂) := by
apply Filter.eventuallyEq_iff_exists_mem.2
use s
constructor
· exact IsOpen.mem_nhds hs hx
· intro z hz
apply partialDeriv_add₂_differentiableAt
exact hf₁ z hz
exact hf₂ z hz
rw [partialDeriv_eventuallyEq this]
have t₃ : DifferentiableAt (partialDeriv Complex.I f₁) x := by
let B₀ := (h₁ x hx).contDiffAt (IsOpen.mem_nhds hs hx)
let A₀ := partialDeriv_contDiffAt B₀ Complex.I
exact A₀.differentiableAt (Submonoid.oneLE.proof_2 ℕ∞)
have t₄ : DifferentiableAt (partialDeriv Complex.I f₂) x := by
let B₀ := (h₂ x hx).contDiffAt (IsOpen.mem_nhds hs hx)
let A₀ := partialDeriv_contDiffAt B₀ Complex.I
exact A₀.differentiableAt (Submonoid.oneLE.proof_2 ℕ∞)
rw [partialDeriv_add₂_differentiableAt t₃ t₄]
-- I am super confused at this point because the tactic 'ring' does not work.
-- I do not understand why. So, I need to do things by hand.
rw [add_assoc]
rw [add_assoc]
rw [add_right_inj (partialDeriv 1 (partialDeriv 1 f₁) x)]
rw [add_comm]
rw [add_assoc]
rw [add_right_inj (partialDeriv Complex.I (partialDeriv Complex.I f₁) x)]
rw [add_comm]
theorem laplace_smul {f : → F} : ∀ v : , Δ (v • f) = v • (Δ f) := by theorem laplace_smul {f : → F} : ∀ v : , Δ (v • f) = v • (Δ f) := by
intro v intro v
unfold Complex.laplace unfold Complex.laplace

View File

@ -85,6 +85,21 @@ theorem partialDeriv_add₂_differentiableAt
rfl rfl
theorem partialDeriv_add₂_differentiableAt'
{f₁ f₂ : E → F}
{v : E}
{x : E}
(h₁ : DifferentiableAt 𝕜 f₁ x)
(h₂ : DifferentiableAt 𝕜 f₂ x) :
partialDeriv 𝕜 v (f₁ + f₂) =ᶠ[nhds x] (partialDeriv 𝕜 v f₁) + (partialDeriv 𝕜 v f₂) := by
unfold partialDeriv
have : f₁ + f₂ = fun y ↦ f₁ y + f₂ y := by rfl
rw [this]
rw [fderiv_add h₁ h₂]
rfl
theorem partialDeriv_compContLin {f : E → F} {l : F →L[𝕜] G} {v : E} (h : Differentiable 𝕜 f) : partialDeriv 𝕜 v (l ∘ f) = l ∘ partialDeriv 𝕜 v f := by 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 unfold partialDeriv