kebekus
/
nevanlinna
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update analyticAt.lean

This commit is contained in:
Stefan Kebekus 2024-09-12 07:04:00 +02:00
parent f83f772506
commit dbea68061b
1 changed files with 8 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
Nevanlinna/analyticAt.lean
View File

@ -123,7 +123,7 @@ theorem eventually_nhds_comp_composition
exact h₁t (ℓ y) hy
· constructor
· apply IsOpen.preimage
exact ContinuousLinearEquiv.continuous ℓ
exact hℓ
exact h₂t
· exact h₃t
@ -132,9 +132,10 @@ theorem AnalyticAt.order_congr
{f₁ f₂ : ℂ → ℂ}
{z₀ : ℂ}
(hf₁ : AnalyticAt ℂ f₁ z₀)
(hf₂ : AnalyticAt ℂ f₂ z₀)
(hf : ∀ᶠ (z : ℂ) in nhds z₀, f₁ z = f₂ z) :
hf₁.order = hf₂.order := by
(hf : f₁ =ᶠ[nhds z₀] f₂) :
hf₁.order = (hf₁.congr hf).order := by
sorry
@ -151,9 +152,9 @@ theorem AnalyticAt.order_comp_CLE
rw [AnalyticAt.order_eq_top_iff] at h₁f
let A := eventually_nhds_comp_composition h₁f ℓ.continuous
simp at A
have : AnalyticAt ℂ (0 : ℂ → ℂ) z₀ := by apply analyticAt_const
rw [AnalyticAt.order_congr (hf.comp (ℓ.analyticAt z₀)) this A]
rw [AnalyticAt.order_congr (hf.comp (ℓ.analyticAt z₀)) A]
have : AnalyticAt ℂ (0 : ℂ → ℂ) z₀ := by apply analyticAt_const
have : this.order = ⊤ := by
rw [AnalyticAt.order_eq_top_iff]
simp
@ -176,7 +177,7 @@ theorem AnalyticAt.order_comp_CLE
exact t₀
apply AnalyticAt.comp h₁g
exact ContinuousLinearEquiv.analyticAt ℓ z₀
rw [AnalyticAt.order_congr (hf.comp (ℓ.analyticAt z₀)) this A]
rw [AnalyticAt.order_congr (hf.comp (ℓ.analyticAt z₀)) A]
simp
rw [AnalyticAt.order_mul t₀ ((h₁g.comp (ℓ.analyticAt z₀)))]