Update analyticAt.lean

This commit is contained in:
Stefan Kebekus 2024-09-12 07:12:03 +02:00
parent dbea68061b
commit b988031047
1 changed files with 18 additions and 4 deletions

View File

@ -135,9 +135,22 @@ theorem AnalyticAt.order_congr
(hf : f₁ =ᶠ[nhds z₀] f₂) :
hf₁.order = (hf₁.congr hf).order := by
sorry
by_cases h₁f₁ : hf₁.order =
rw [h₁f₁, eq_comm, AnalyticAt.order_eq_top_iff]
rw [AnalyticAt.order_eq_top_iff] at h₁f₁
exact Filter.EventuallyEq.rw h₁f₁ (fun x => Eq (f₂ x)) (id (Filter.EventuallyEq.symm hf))
--
let n := hf₁.order.toNat
have hn : hf₁.order = n := Eq.symm (ENat.coe_toNat h₁f₁)
rw [hn, eq_comm, AnalyticAt.order_eq_nat_iff]
rw [AnalyticAt.order_eq_nat_iff] at hn
obtain ⟨g, h₁g, h₂g, h₃g⟩ := hn
use g
constructor
· assumption
· constructor
· assumption
· exact Filter.EventuallyEq.rw h₃g (fun x => Eq (f₂ x)) (id (Filter.EventuallyEq.symm hf))
theorem AnalyticAt.order_comp_CLE
@ -154,7 +167,8 @@ theorem AnalyticAt.order_comp_CLE
simp at A
rw [AnalyticAt.order_congr (hf.comp (.analyticAt z₀)) A]
have : AnalyticAt (0 : ) z₀ := by apply analyticAt_const
have : AnalyticAt (0 : ) z₀ := by
apply analyticAt_const
have : this.order = := by
rw [AnalyticAt.order_eq_top_iff]
simp