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

Fix compilation

Browse Source
This commit is contained in:
Stefan Kebekus 2024-12-03 08:00:55 +01:00
parent 084841c35a
commit 9aa2604c18
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
Nevanlinna/harmonicAt.lean
View File

@ -22,7 +22,7 @@ theorem HarmonicAt_iff
HarmonicAt f x ↔ ∃ s : Set ℂ, IsOpen s ∧ x ∈ s ∧ (ContDiffOn ℝ 2 f s) ∧ (∀ z ∈ s, Δ f z = 0) := by HarmonicAt f x ↔ ∃ s : Set ℂ, IsOpen s ∧ x ∈ s ∧ (ContDiffOn ℝ 2 f s) ∧ (∀ z ∈ s, Δ f z = 0) := by
constructor constructor
· intro hf · intro hf
obtain ⟨s₁, h₁s₁, h₂s₁, h₃s₁⟩ := hf.1.contDiffOn' le_rfl obtain ⟨s₁, h₁s₁, h₂s₁, h₃s₁⟩ := hf.1.contDiffOn' le_rfl (by trivial)
simp at h₃s₁ simp at h₃s₁
obtain ⟨t₂, h₁t₂, h₂t₂⟩ := (Filter.eventuallyEq_iff_exists_mem.1 hf.2) obtain ⟨t₂, h₁t₂, h₂t₂⟩ := (Filter.eventuallyEq_iff_exists_mem.1 hf.2)
obtain ⟨s₂, h₁s₂, h₂s₂, h₃s₂⟩ := mem_nhds_iff.1 h₁t₂ obtain ⟨s₂, h₁s₂, h₂s₂, h₃s₂⟩ := mem_nhds_iff.1 h₁t₂
@ -261,7 +261,7 @@ theorem harmonicAt_comp_CLM_is_harmonicAt
apply ContDiffAt.continuousLinearMap_comp apply ContDiffAt.continuousLinearMap_comp
exact h.1 exact h.1
· -- Δ (⇑l ∘ f) =ᶠ[nhds z] 0 · -- Δ (⇑l ∘ f) =ᶠ[nhds z] 0
obtain ⟨r, h₁r, h₂r⟩ := h.1.contDiffOn le_rfl obtain ⟨r, h₁r, h₂r⟩ := h.1.contDiffOn le_rfl (by trivial)
obtain ⟨s, h₁s, h₂s, h₃s⟩ := mem_nhds_iff.1 h₁r obtain ⟨s, h₁s, h₂s, h₃s⟩ := mem_nhds_iff.1 h₁r
obtain ⟨t, h₁t, h₂t⟩ := Filter.eventuallyEq_iff_exists_mem.1 h.2 obtain ⟨t, h₁t, h₂t⟩ := Filter.eventuallyEq_iff_exists_mem.1 h.2
obtain ⟨u, h₁u, h₂u, h₃u⟩ := mem_nhds_iff.1 h₁t obtain ⟨u, h₁u, h₂u, h₃u⟩ := mem_nhds_iff.1 h₁t