This commit is contained in:
Stefan Kebekus 2024-07-30 10:52:12 +02:00
parent 4ca5f6d4d2
commit a2c2d05789
2 changed files with 83 additions and 39 deletions

View File

@ -114,56 +114,86 @@ theorem harmonic_is_realOfHolomorphic
let g : := f_1 - Complex.I • f_I
have reg₀ : Differentiable g := by
let smulICLM : ≃L[] :=
{
toFun := fun x ↦ Complex.I • x
map_add' := fun x y => DistribSMul.smul_add Complex.I x y
map_smul' := fun m x => (smul_comm ((RingHom.id ) m) Complex.I x).symm
invFun := fun x ↦ (Complex.I)⁻¹ • x
left_inv := by
intro x
simp
rw [← mul_assoc, mul_comm]
simp
right_inv := by
intro x
simp
rw [← mul_assoc]
simp
continuous_toFun := continuous_const_smul Complex.I
continuous_invFun := continuous_const_smul (Complex.I)⁻¹
}
apply Differentiable.sub
apply Differentiable.comp
exact ContinuousLinearMap.differentiable Complex.ofRealCLM
have reg₂f : ContDiff 2 f := by
apply contDiff_iff_contDiffAt.mpr
intro z
sorry
apply Differentiable.comp
sorry
sorry
exact (hf z).1
have reg₁f_1 : ContDiff 1 f_1 := by
apply contDiff_iff_contDiffAt.mpr
intro z
dsimp [f_1]
apply ContDiffAt.continuousLinearMap_comp
exact partialDeriv_contDiffAt (hf z).1 1
have reg₁f_I : ContDiff 1 f_I := by
apply contDiff_iff_contDiffAt.mpr
intro z
dsimp [f_I]
apply ContDiffAt.continuousLinearMap_comp
exact partialDeriv_contDiffAt (hf z).1 Complex.I
have reg₁g : ContDiff 1 g := by
dsimp [g]
apply ContDiff.sub
exact reg₁f_1
have : Complex.I • f_I = fun x ↦ Complex.I • f_I x := rfl
rw [this]
apply ContDiff.const_smul
exact reg₁f_I
have reg₁ : Differentiable g := by
intro z
apply CauchyRiemann₇.2
constructor
· exact reg₀ z
· apply Differentiable.differentiableAt
apply ContDiff.differentiable
exact reg₁g
rfl
· dsimp [g]
have : f_1 - Complex.I • f_I = f_1 + (- Complex.I • f_I) := by
rw [sub_eq_add_neg]
simp
rw [this, partialDeriv_add₂, partialDeriv_add₂]
rw [partialDeriv_sub₂, partialDeriv_sub₂]
simp
dsimp [f_1, f_I]
sorry
sorry
sorry
sorry
sorry
rw [partialDeriv_smul'₂, partialDeriv_smul'₂]
rw [partialDeriv_compContLin, partialDeriv_compContLin, partialDeriv_compContLin, partialDeriv_compContLin]
rw [mul_sub]
simp
rw [← mul_assoc]
simp
rw [add_comm, sub_eq_add_neg]
congr 1
· rw [partialDeriv_comm reg₂f Complex.I 1]
· let A := Filter.EventuallyEq.eq_of_nhds (hf z).2
simp at A
unfold Complex.laplace at A
conv =>
right
right
rw [← sub_zero (partialDeriv 1 (partialDeriv 1 f) z)]
rw [← A]
simp
--Differentiable (partialDeriv _ f)
repeat
apply ContDiff.differentiable
apply contDiff_iff_contDiffAt.mpr
exact fun w ↦ partialDeriv_contDiffAt (hf w).1 _
apply le_rfl
-- Differentiable f_1
exact reg₁f_1.differentiable le_rfl
-- Differentiable (Complex.I • f_I)
have : Complex.I • f_I = fun x ↦ Complex.I • f_I x := rfl
rw [this]
apply Differentiable.const_smul
exact reg₁f_I.differentiable le_rfl
-- Differentiable f_1
exact reg₁f_1.differentiable le_rfl
-- Differentiable (Complex.I • f_I)
have : Complex.I • f_I = fun x ↦ Complex.I • f_I x := rfl
rw [this]
apply Differentiable.const_smul
exact reg₁f_I.differentiable le_rfl

View File

@ -102,6 +102,20 @@ theorem partialDeriv_add₂ {f₁ f₂ : E → F} (h₁ : Differentiable 𝕜 f
simp
theorem partialDeriv_sub₂ {f₁ f₂ : E → F} (h₁ : Differentiable 𝕜 f₁) (h₂ : Differentiable 𝕜 f₂) : ∀ v : E, partialDeriv 𝕜 v (f₁ - f₂) = (partialDeriv 𝕜 v f₁) - (partialDeriv 𝕜 v f₂) := by
unfold partialDeriv
intro v
have : f₁ - f₂ = fun y ↦ f₁ y - f₂ y := by rfl
rw [this]
conv =>
left
intro w
left
rw [fderiv_sub (h₁ w) (h₂ w)]
funext w
simp
theorem partialDeriv_add₂_differentiableAt
{f₁ f₂ : E → F}
{v : E}