Compare commits
No commits in common. "main" and "feature/analyticOn" have entirely different histories.
main
...
feature/an
|
|
@ -2,20 +2,6 @@ import Mathlib.Analysis.Analytic.IsolatedZeros
|
|||
import Mathlib.Analysis.Complex.Basic
|
||||
import Mathlib.Analysis.Analytic.Linear
|
||||
|
||||
open Topology
|
||||
|
||||
|
||||
theorem AnalyticAt.order_neq_top_iff
|
||||
{f : ℂ → ℂ}
|
||||
{z₀ : ℂ}
|
||||
(hf : AnalyticAt ℂ f z₀) :
|
||||
hf.order ≠ ⊤ ↔ ∃ (g : ℂ → ℂ), AnalyticAt ℂ g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds z₀, f z = (z - z₀) ^ (hf.order.toNat) • g z := by
|
||||
rw [← hf.order_eq_nat_iff]
|
||||
constructor
|
||||
· intro h₁f
|
||||
exact Eq.symm (ENat.coe_toNat h₁f)
|
||||
· intro h₁f
|
||||
exact ENat.coe_toNat_eq_self.mp (id (Eq.symm h₁f))
|
||||
|
||||
|
||||
theorem AnalyticAt.order_mul
|
||||
|
|
@ -119,6 +105,10 @@ theorem AnalyticAt.supp_order_toNat
|
|||
simp [hf.order_eq_zero_iff.2 h₁f]
|
||||
|
||||
|
||||
theorem ContinuousLinearEquiv.analyticAt
|
||||
(ℓ : ℂ ≃L[ℂ] ℂ) (z₀ : ℂ) : AnalyticAt ℂ (⇑ℓ) z₀ := ℓ.toContinuousLinearMap.analyticAt z₀
|
||||
|
||||
|
||||
theorem eventually_nhds_comp_composition
|
||||
{f₁ f₂ ℓ : ℂ → ℂ}
|
||||
{z₀ : ℂ}
|
||||
|
|
@ -234,111 +224,3 @@ theorem AnalyticAt.order_comp_CLE
|
|||
rw [this]
|
||||
|
||||
simp
|
||||
|
||||
|
||||
theorem AnalyticAt.localIdentity
|
||||
{f g : ℂ → ℂ}
|
||||
{z₀ : ℂ}
|
||||
(hf : AnalyticAt ℂ f z₀)
|
||||
(hg : AnalyticAt ℂ g z₀) :
|
||||
f =ᶠ[𝓝[≠] z₀] g → f =ᶠ[𝓝 z₀] g := by
|
||||
intro h
|
||||
let Δ := f - g
|
||||
have : AnalyticAt ℂ Δ z₀ := AnalyticAt.sub hf hg
|
||||
have t₁ : Δ =ᶠ[𝓝[≠] z₀] 0 := by
|
||||
exact Filter.eventuallyEq_iff_sub.mp h
|
||||
|
||||
have : Δ =ᶠ[𝓝 z₀] 0 := by
|
||||
rcases (AnalyticAt.eventually_eq_zero_or_eventually_ne_zero this) with h | h
|
||||
· exact h
|
||||
· have := Filter.EventuallyEq.eventually t₁
|
||||
let A := Filter.eventually_and.2 ⟨this, h⟩
|
||||
let _ := Filter.Eventually.exists A
|
||||
tauto
|
||||
exact Filter.eventuallyEq_iff_sub.mpr this
|
||||
|
||||
|
||||
theorem AnalyticAt.mul₁
|
||||
{f g : ℂ → ℂ}
|
||||
{z : ℂ}
|
||||
(hf : AnalyticAt ℂ f z)
|
||||
(hg : AnalyticAt ℂ g z) :
|
||||
AnalyticAt ℂ (f * g) z := by
|
||||
rw [(by rfl : f * g = (fun x ↦ f x * g x))]
|
||||
exact mul hf hg
|
||||
|
||||
|
||||
theorem analyticAt_finprod
|
||||
{α : Type}
|
||||
{f : α → ℂ → ℂ}
|
||||
{z : ℂ}
|
||||
(hf : ∀ a, AnalyticAt ℂ (f a) z) :
|
||||
AnalyticAt ℂ (∏ᶠ a, f a) z := by
|
||||
by_cases h₁f : (Function.mulSupport f).Finite
|
||||
· rw [finprod_eq_prod f h₁f]
|
||||
rw [Finset.prod_fn h₁f.toFinset f]
|
||||
exact Finset.analyticAt_prod h₁f.toFinset (fun a _ ↦ hf a)
|
||||
· rw [finprod_of_infinite_mulSupport h₁f]
|
||||
exact analyticAt_const
|
||||
|
||||
|
||||
lemma AnalyticAt.zpow_nonneg
|
||||
{f : ℂ → ℂ}
|
||||
{z₀ : ℂ}
|
||||
{n : ℤ}
|
||||
(hf : AnalyticAt ℂ f z₀)
|
||||
(hn : 0 ≤ n) :
|
||||
AnalyticAt ℂ (fun x ↦ (f x) ^ n) z₀ := by
|
||||
simp_rw [(Eq.symm (Int.toNat_of_nonneg hn) : n = OfNat.ofNat n.toNat), zpow_ofNat]
|
||||
apply AnalyticAt.pow hf
|
||||
|
||||
|
||||
theorem AnalyticAt.zpow
|
||||
{f : ℂ → ℂ}
|
||||
{z₀ : ℂ}
|
||||
{n : ℤ}
|
||||
(h₁f : AnalyticAt ℂ f z₀)
|
||||
(h₂f : f z₀ ≠ 0) :
|
||||
AnalyticAt ℂ (fun x ↦ (f x) ^ n) z₀ := by
|
||||
by_cases hn : 0 ≤ n
|
||||
· exact zpow_nonneg h₁f hn
|
||||
· rw [(Int.eq_neg_comm.mp rfl : n = - (- n))]
|
||||
conv =>
|
||||
arg 2
|
||||
intro x
|
||||
rw [zpow_neg]
|
||||
exact AnalyticAt.inv (zpow_nonneg h₁f (by linarith)) (zpow_ne_zero (-n) h₂f)
|
||||
|
||||
|
||||
/- A function is analytic at a point iff it is analytic after multiplication
|
||||
with a non-vanishing analytic function
|
||||
-/
|
||||
theorem analyticAt_of_mul_analytic
|
||||
{f g : ℂ → ℂ}
|
||||
{z₀ : ℂ}
|
||||
(h₁g : AnalyticAt ℂ g z₀)
|
||||
(h₂g : g z₀ ≠ 0) :
|
||||
AnalyticAt ℂ f z₀ ↔ AnalyticAt ℂ (f * g) z₀ := by
|
||||
constructor
|
||||
· exact fun a => AnalyticAt.mul₁ a h₁g
|
||||
· intro hprod
|
||||
|
||||
let g' := fun z ↦ (g z)⁻¹
|
||||
have h₁g' := h₁g.inv h₂g
|
||||
have h₂g' : g' z₀ ≠ 0 := by
|
||||
exact inv_ne_zero h₂g
|
||||
|
||||
have : f =ᶠ[𝓝 z₀] f * g * fun x => (g x)⁻¹ := by
|
||||
unfold Filter.EventuallyEq
|
||||
apply Filter.eventually_iff_exists_mem.mpr
|
||||
use g⁻¹' {0}ᶜ
|
||||
constructor
|
||||
· apply ContinuousAt.preimage_mem_nhds
|
||||
exact AnalyticAt.continuousAt h₁g
|
||||
exact compl_singleton_mem_nhds_iff.mpr h₂g
|
||||
· intro y hy
|
||||
simp at hy
|
||||
simp [hy]
|
||||
rw [analyticAt_congr this]
|
||||
apply hprod.mul
|
||||
exact h₁g'
|
||||
|
|
|
|||
|
|
@ -1,59 +0,0 @@
|
|||
import Nevanlinna.analyticAt
|
||||
import Nevanlinna.divisor
|
||||
|
||||
open scoped Interval Topology
|
||||
open Real Filter MeasureTheory intervalIntegral
|
||||
|
||||
|
||||
noncomputable def AnalyticOnNhd.zeroDivisor
|
||||
{f : ℂ → ℂ}
|
||||
{U : Set ℂ}
|
||||
(hf : AnalyticOnNhd ℂ f U) :
|
||||
Divisor U where
|
||||
|
||||
toFun := by
|
||||
intro z
|
||||
if hz : z ∈ U then
|
||||
exact ((hf z hz).order.toNat : ℤ)
|
||||
else
|
||||
exact 0
|
||||
|
||||
supportInU := by
|
||||
intro z hz
|
||||
simp at hz
|
||||
by_contra h₂z
|
||||
simp [h₂z] at hz
|
||||
|
||||
locallyFiniteInU := by
|
||||
intro z hz
|
||||
|
||||
apply eventually_nhdsWithin_iff.2
|
||||
rw [eventually_nhds_iff]
|
||||
|
||||
rcases AnalyticAt.eventually_eq_zero_or_eventually_ne_zero (hf z hz) with h|h
|
||||
· rw [eventually_nhds_iff] at h
|
||||
obtain ⟨N, h₁N, h₂N, h₃N⟩ := h
|
||||
use N
|
||||
constructor
|
||||
· intro y h₁y _
|
||||
by_cases h₃y : y ∈ U
|
||||
· simp [h₃y]
|
||||
right
|
||||
rw [AnalyticAt.order_eq_top_iff (hf y h₃y)]
|
||||
rw [eventually_nhds_iff]
|
||||
use N
|
||||
· simp [h₃y]
|
||||
· tauto
|
||||
|
||||
· rw [eventually_nhdsWithin_iff, eventually_nhds_iff] at h
|
||||
obtain ⟨N, h₁N, h₂N, h₃N⟩ := h
|
||||
use N
|
||||
constructor
|
||||
· intro y h₁y h₂y
|
||||
by_cases h₃y : y ∈ U
|
||||
· simp [h₃y]
|
||||
left
|
||||
rw [AnalyticAt.order_eq_zero_iff (hf y h₃y)]
|
||||
exact h₁N y h₁y h₂y
|
||||
· simp [h₃y]
|
||||
· tauto
|
||||
|
|
@ -4,17 +4,17 @@ import Mathlib.Analysis.Complex.Basic
|
|||
import Nevanlinna.analyticAt
|
||||
|
||||
|
||||
noncomputable def AnalyticOnNhd.order
|
||||
{f : ℂ → ℂ} {U : Set ℂ} (hf : AnalyticOnNhd ℂ f U) : U → ℕ∞ := fun u ↦ (hf u u.2).order
|
||||
noncomputable def AnalyticOn.order
|
||||
{f : ℂ → ℂ} {U : Set ℂ} (hf : AnalyticOn ℂ f U) : U → ℕ∞ := fun u ↦ (hf u u.2).order
|
||||
|
||||
|
||||
theorem AnalyticOnNhd.order_eq_nat_iff
|
||||
theorem AnalyticOn.order_eq_nat_iff
|
||||
{f : ℂ → ℂ}
|
||||
{U : Set ℂ}
|
||||
{z₀ : U}
|
||||
(hf : AnalyticOnNhd ℂ f U)
|
||||
(hf : AnalyticOn ℂ f U)
|
||||
(n : ℕ) :
|
||||
hf.order z₀ = ↑n ↔ ∃ (g : ℂ → ℂ), AnalyticOnNhd ℂ g U ∧ g z₀ ≠ 0 ∧ ∀ z, f z = (z - z₀) ^ n • g z := by
|
||||
hf.order z₀ = ↑n ↔ ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ g z₀ ≠ 0 ∧ ∀ z, f z = (z - z₀) ^ n • g z := by
|
||||
|
||||
constructor
|
||||
-- Direction →
|
||||
|
|
@ -91,31 +91,31 @@ theorem AnalyticOnNhd.order_eq_nat_iff
|
|||
-- direction ←
|
||||
intro h
|
||||
obtain ⟨g, h₁g, h₂g, h₃g⟩ := h
|
||||
dsimp [AnalyticOnNhd.order]
|
||||
dsimp [AnalyticOn.order]
|
||||
rw [AnalyticAt.order_eq_nat_iff]
|
||||
use g
|
||||
exact ⟨h₁g z₀ z₀.2, ⟨h₂g, Filter.Eventually.of_forall h₃g⟩⟩
|
||||
|
||||
|
||||
theorem AnalyticOnNhd.support_of_order₁
|
||||
theorem AnalyticOn.support_of_order₁
|
||||
{f : ℂ → ℂ}
|
||||
{U : Set ℂ}
|
||||
(hf : AnalyticOnNhd ℂ f U) :
|
||||
(hf : AnalyticOn ℂ f U) :
|
||||
Function.support hf.order = U.restrict f⁻¹' {0} := by
|
||||
ext u
|
||||
simp [AnalyticOnNhd.order]
|
||||
simp [AnalyticOn.order]
|
||||
rw [not_iff_comm, (hf u u.2).order_eq_zero_iff]
|
||||
|
||||
|
||||
theorem AnalyticOnNhd.eliminateZeros
|
||||
theorem AnalyticOn.eliminateZeros
|
||||
{f : ℂ → ℂ}
|
||||
{U : Set ℂ}
|
||||
{A : Finset U}
|
||||
(hf : AnalyticOnNhd ℂ f U)
|
||||
(hf : AnalyticOn ℂ f U)
|
||||
(n : U → ℕ) :
|
||||
(∀ a ∈ A, hf.order a = n a) → ∃ (g : ℂ → ℂ), AnalyticOnNhd ℂ g U ∧ (∀ a ∈ A, g a ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (n a)) • g z := by
|
||||
(∀ a ∈ A, hf.order a = n a) → ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ (∀ a ∈ A, g a ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (n a)) • g z := by
|
||||
|
||||
apply Finset.induction (α := U) (p := fun A ↦ (∀ a ∈ A, (hf a.1 a.2).order = n a) → ∃ (g : ℂ → ℂ), AnalyticOnNhd ℂ g U ∧ (∀ a ∈ A, g a ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (n a)) • g z)
|
||||
apply Finset.induction (α := U) (p := fun A ↦ (∀ a ∈ A, (hf a.1 a.2).order = n a) → ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ (∀ a ∈ A, g a ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (n a)) • g z)
|
||||
|
||||
-- case empty
|
||||
simp
|
||||
|
|
@ -146,7 +146,7 @@ theorem AnalyticOnNhd.eliminateZeros
|
|||
intro b _
|
||||
apply AnalyticAt.pow
|
||||
apply AnalyticAt.sub
|
||||
apply analyticAt_id
|
||||
apply analyticAt_id ℂ
|
||||
exact analyticAt_const
|
||||
|
||||
have h₂φ : h₁φ.order = (0 : ℕ) := by
|
||||
|
|
@ -173,7 +173,7 @@ theorem AnalyticOnNhd.eliminateZeros
|
|||
rw [h₂φ]
|
||||
simp
|
||||
|
||||
obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (AnalyticOnNhd.order_eq_nat_iff h₁g₀ (n b₀)).1 this
|
||||
obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (AnalyticOn.order_eq_nat_iff h₁g₀ (n b₀)).1 this
|
||||
|
||||
use g₁
|
||||
constructor
|
||||
|
|
@ -203,7 +203,7 @@ theorem XX
|
|||
{f : ℂ → ℂ}
|
||||
{U : Set ℂ}
|
||||
(hU : IsPreconnected U)
|
||||
(h₁f : AnalyticOnNhd ℂ f U)
|
||||
(h₁f : AnalyticOn ℂ f U)
|
||||
(h₂f : ∃ u ∈ U, f u ≠ 0) :
|
||||
∀ (hu : u ∈ U), (h₁f u hu).order.toNat = (h₁f u hu).order := by
|
||||
|
||||
|
|
@ -221,7 +221,7 @@ theorem discreteZeros
|
|||
{f : ℂ → ℂ}
|
||||
{U : Set ℂ}
|
||||
(hU : IsPreconnected U)
|
||||
(h₁f : AnalyticOnNhd ℂ f U)
|
||||
(h₁f : AnalyticOn ℂ f U)
|
||||
(h₂f : ∃ u ∈ U, f u ≠ 0) :
|
||||
DiscreteTopology ((U.restrict f)⁻¹' {0}) := by
|
||||
|
||||
|
|
@ -293,7 +293,7 @@ theorem finiteZeros
|
|||
{U : Set ℂ}
|
||||
(h₁U : IsPreconnected U)
|
||||
(h₂U : IsCompact U)
|
||||
(h₁f : AnalyticOnNhd ℂ f U)
|
||||
(h₁f : AnalyticOn ℂ f U)
|
||||
(h₂f : ∃ u ∈ U, f u ≠ 0) :
|
||||
Set.Finite (U.restrict f⁻¹' {0}) := by
|
||||
|
||||
|
|
@ -310,14 +310,14 @@ theorem finiteZeros
|
|||
exact discreteZeros h₁U h₁f h₂f
|
||||
|
||||
|
||||
theorem AnalyticOnNhdCompact.eliminateZeros
|
||||
theorem AnalyticOnCompact.eliminateZeros
|
||||
{f : ℂ → ℂ}
|
||||
{U : Set ℂ}
|
||||
(h₁U : IsPreconnected U)
|
||||
(h₂U : IsCompact U)
|
||||
(h₁f : AnalyticOnNhd ℂ f U)
|
||||
(h₁f : AnalyticOn ℂ f U)
|
||||
(h₂f : ∃ u ∈ U, f u ≠ 0) :
|
||||
∃ (g : ℂ → ℂ) (A : Finset U), AnalyticOnNhd ℂ g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (h₁f.order a).toNat) • g z := by
|
||||
∃ (g : ℂ → ℂ) (A : Finset U), AnalyticOn ℂ g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (h₁f.order a).toNat) • g z := by
|
||||
|
||||
let A := (finiteZeros h₁U h₂U h₁f h₂f).toFinset
|
||||
|
||||
|
|
@ -325,13 +325,13 @@ theorem AnalyticOnNhdCompact.eliminateZeros
|
|||
|
||||
have hn : ∀ a ∈ A, (h₁f a a.2).order = n a := by
|
||||
intro a _
|
||||
dsimp [n, AnalyticOnNhd.order]
|
||||
dsimp [n, AnalyticOn.order]
|
||||
rw [eq_comm]
|
||||
apply XX h₁U
|
||||
exact h₂f
|
||||
|
||||
|
||||
obtain ⟨g, h₁g, h₂g, h₃g⟩ := AnalyticOnNhd.eliminateZeros (A := A) h₁f n hn
|
||||
obtain ⟨g, h₁g, h₂g, h₃g⟩ := AnalyticOn.eliminateZeros (A := A) h₁f n hn
|
||||
use g
|
||||
use A
|
||||
|
||||
|
|
@ -357,14 +357,14 @@ theorem AnalyticOnNhdCompact.eliminateZeros
|
|||
· exact inter
|
||||
|
||||
|
||||
theorem AnalyticOnNhdCompact.eliminateZeros₂
|
||||
theorem AnalyticOnCompact.eliminateZeros₂
|
||||
{f : ℂ → ℂ}
|
||||
{U : Set ℂ}
|
||||
(h₁U : IsPreconnected U)
|
||||
(h₂U : IsCompact U)
|
||||
(h₁f : AnalyticOnNhd ℂ f U)
|
||||
(h₁f : AnalyticOn ℂ f U)
|
||||
(h₂f : ∃ u ∈ U, f u ≠ 0) :
|
||||
∃ (g : ℂ → ℂ), AnalyticOnNhd ℂ g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ a ∈ (finiteZeros h₁U h₂U h₁f h₂f).toFinset, (z - a) ^ (h₁f.order a).toNat) • g z := by
|
||||
∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ a ∈ (finiteZeros h₁U h₂U h₁f h₂f).toFinset, (z - a) ^ (h₁f.order a).toNat) • g z := by
|
||||
|
||||
let A := (finiteZeros h₁U h₂U h₁f h₂f).toFinset
|
||||
|
||||
|
|
@ -372,12 +372,12 @@ theorem AnalyticOnNhdCompact.eliminateZeros₂
|
|||
|
||||
have hn : ∀ a ∈ A, (h₁f a a.2).order = n a := by
|
||||
intro a _
|
||||
dsimp [n, AnalyticOnNhd.order]
|
||||
dsimp [n, AnalyticOn.order]
|
||||
rw [eq_comm]
|
||||
apply XX h₁U
|
||||
exact h₂f
|
||||
|
||||
obtain ⟨g, h₁g, h₂g, h₃g⟩ := AnalyticOnNhd.eliminateZeros (A := A) h₁f n hn
|
||||
obtain ⟨g, h₁g, h₂g, h₃g⟩ := AnalyticOn.eliminateZeros (A := A) h₁f n hn
|
||||
use g
|
||||
|
||||
have inter : ∀ (z : ℂ), f z = (∏ a ∈ A, (z - ↑a) ^ (h₁f (↑a) a.property).order.toNat) • g z := by
|
||||
|
|
@ -402,14 +402,14 @@ theorem AnalyticOnNhdCompact.eliminateZeros₂
|
|||
· exact h₃g
|
||||
|
||||
|
||||
theorem AnalyticOnNhdCompact.eliminateZeros₁
|
||||
theorem AnalyticOnCompact.eliminateZeros₁
|
||||
{f : ℂ → ℂ}
|
||||
{U : Set ℂ}
|
||||
(h₁U : IsPreconnected U)
|
||||
(h₂U : IsCompact U)
|
||||
(h₁f : AnalyticOnNhd ℂ f U)
|
||||
(h₁f : AnalyticOn ℂ f U)
|
||||
(h₂f : ∃ u ∈ U, f u ≠ 0) :
|
||||
∃ (g : ℂ → ℂ), AnalyticOnNhd ℂ g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ᶠ a, (z - a) ^ (h₁f.order a).toNat) • g z := by
|
||||
∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ᶠ a, (z - a) ^ (h₁f.order a).toNat) • g z := by
|
||||
|
||||
let A := (finiteZeros h₁U h₂U h₁f h₂f).toFinset
|
||||
|
||||
|
|
@ -417,12 +417,12 @@ theorem AnalyticOnNhdCompact.eliminateZeros₁
|
|||
|
||||
have hn : ∀ a ∈ A, (h₁f a a.2).order = n a := by
|
||||
intro a _
|
||||
dsimp [n, AnalyticOnNhd.order]
|
||||
dsimp [n, AnalyticOn.order]
|
||||
rw [eq_comm]
|
||||
apply XX h₁U
|
||||
exact h₂f
|
||||
|
||||
obtain ⟨g, h₁g, h₂g, h₃g⟩ := AnalyticOnNhd.eliminateZeros (A := A) h₁f n hn
|
||||
obtain ⟨g, h₁g, h₂g, h₃g⟩ := AnalyticOn.eliminateZeros (A := A) h₁f n hn
|
||||
use g
|
||||
|
||||
have inter : ∀ (z : ℂ), f z = (∏ a ∈ A, (z - ↑a) ^ (h₁f (↑a) a.property).order.toNat) • g z := by
|
||||
|
|
@ -28,7 +28,7 @@ orthonormal basis `v` as `∑ i, (v i) ⊗ₜ[ℝ] (v i)`.
|
|||
|
||||
-/
|
||||
|
||||
open InnerProductSpace
|
||||
|
||||
open TensorProduct
|
||||
|
||||
|
||||
|
|
@ -41,11 +41,12 @@ noncomputable def InnerProductSpace.canonicalCovariantTensor
|
|||
(E : Type*) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
|
||||
: E ⊗[ℝ] E := ∑ i, ((stdOrthonormalBasis ℝ E) i) ⊗ₜ[ℝ] ((stdOrthonormalBasis ℝ E) i)
|
||||
|
||||
|
||||
theorem InnerProductSpace.canonicalCovariantTensorRepresentation
|
||||
(E : Type*) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
|
||||
[Fintype ι]
|
||||
(v : OrthonormalBasis ι ℝ E) :
|
||||
InnerProductSpace.canonicalCovariantTensor E = ∑ i, (v i) ⊗ₜ[ℝ] (v i) := by
|
||||
(v : OrthonormalBasis ι ℝ E)
|
||||
: InnerProductSpace.canonicalCovariantTensor E = ∑ i, (v i) ⊗ₜ[ℝ] (v i) := by
|
||||
|
||||
let w := stdOrthonormalBasis ℝ E
|
||||
conv =>
|
||||
|
|
|
|||
|
|
@ -31,7 +31,7 @@ theorem CauchyRiemann₃ : (DifferentiableAt ℂ f z)
|
|||
have ContinuousLinearMap.comp_lineDeriv : ∀ w : ℂ, ∀ l : ℂ →L[ℝ] ℝ, lineDeriv ℝ (l ∘ f) z w = l ((fderiv ℝ f z) w) := by
|
||||
intro w l
|
||||
rw [DifferentiableAt.lineDeriv_eq_fderiv]
|
||||
rw [fderiv_comp]
|
||||
rw [fderiv.comp]
|
||||
simp
|
||||
fun_prop
|
||||
exact h.restrictScalars ℝ
|
||||
|
|
|
|||
|
|
@ -1,93 +0,0 @@
|
|||
import Mathlib.Analysis.SpecialFunctions.Integrals
|
||||
import Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
|
||||
import Mathlib.Analysis.Convex.SpecificFunctions.Deriv
|
||||
import Nevanlinna.analyticAt
|
||||
import Nevanlinna.mathlibAddOn
|
||||
|
||||
open Interval Topology
|
||||
open Real Filter MeasureTheory intervalIntegral
|
||||
|
||||
|
||||
structure Divisor
|
||||
(U : Set ℂ)
|
||||
where
|
||||
toFun : ℂ → ℤ
|
||||
supportInU : toFun.support ⊆ U
|
||||
locallyFiniteInU : ∀ x ∈ U, toFun =ᶠ[𝓝[≠] x] 0
|
||||
|
||||
instance
|
||||
(U : Set ℂ) :
|
||||
CoeFun (Divisor U) (fun _ ↦ ℂ → ℤ) where
|
||||
coe := Divisor.toFun
|
||||
|
||||
attribute [coe] Divisor.toFun
|
||||
|
||||
|
||||
theorem Divisor.discreteSupport
|
||||
{U : Set ℂ}
|
||||
(hU : IsClosed U)
|
||||
(D : Divisor U) :
|
||||
DiscreteTopology D.toFun.support := by
|
||||
apply discreteTopology_subtype_iff.mpr
|
||||
intro x hx
|
||||
apply inf_principal_eq_bot.mpr
|
||||
by_cases h₁x : x ∈ U
|
||||
· let A := D.locallyFiniteInU x h₁x
|
||||
refine mem_nhdsWithin.mpr ?_
|
||||
rw [eventuallyEq_nhdsWithin_iff] at A
|
||||
obtain ⟨U, h₁U, h₂U, h₃U⟩ := eventually_nhds_iff.1 A
|
||||
use U
|
||||
constructor
|
||||
· exact h₂U
|
||||
· constructor
|
||||
· exact h₃U
|
||||
· intro y hy
|
||||
let C := h₁U y hy.1 hy.2
|
||||
tauto
|
||||
· refine mem_nhdsWithin.mpr ?_
|
||||
use Uᶜ
|
||||
constructor
|
||||
· simpa
|
||||
· constructor
|
||||
· tauto
|
||||
· intro y _
|
||||
let A := D.supportInU
|
||||
simp at A
|
||||
simp
|
||||
exact False.elim (h₁x (A x hx))
|
||||
|
||||
|
||||
|
||||
theorem Divisor.closedSupport
|
||||
{U : Set ℂ}
|
||||
(hU : IsClosed U)
|
||||
(D : Divisor U) :
|
||||
IsClosed D.toFun.support := by
|
||||
|
||||
rw [← isOpen_compl_iff]
|
||||
rw [isOpen_iff_eventually]
|
||||
intro x hx
|
||||
by_cases h₁x : x ∈ U
|
||||
· have A := D.locallyFiniteInU x h₁x
|
||||
simp [A]
|
||||
simp at hx
|
||||
let B := Mnhds A hx
|
||||
simpa
|
||||
· rw [eventually_iff_exists_mem]
|
||||
use Uᶜ
|
||||
constructor
|
||||
· exact IsClosed.compl_mem_nhds hU h₁x
|
||||
· intro y hy
|
||||
simp
|
||||
exact Function.nmem_support.mp fun a => hy (D.supportInU a)
|
||||
|
||||
|
||||
theorem Divisor.finiteSupport
|
||||
{U : Set ℂ}
|
||||
(hU : IsCompact U)
|
||||
(D : Divisor U) :
|
||||
Set.Finite D.toFun.support := by
|
||||
apply IsCompact.finite
|
||||
· apply IsCompact.of_isClosed_subset hU (D.closedSupport hU.isClosed)
|
||||
exact D.supportInU
|
||||
· exact D.discreteSupport hU.isClosed
|
||||
|
|
@ -1,19 +1,15 @@
|
|||
import Mathlib.Analysis.Analytic.Meromorphic
|
||||
import Nevanlinna.holomorphic_JensenFormula
|
||||
|
||||
open Real
|
||||
|
||||
variable (f : ℂ → ℂ)
|
||||
variable {h₁f : MeromorphicOn f ⊤}
|
||||
variable {f : ℂ → ℂ}
|
||||
variable {h₁f : AnalyticOn ℂ f ⊤}
|
||||
variable {h₂f : f 0 ≠ 0}
|
||||
|
||||
|
||||
|
||||
noncomputable def Nevanlinna.n : ℝ → ℤ := by
|
||||
noncomputable def unintegratedCounting : ℝ → ℕ := by
|
||||
intro r
|
||||
have : MeromorphicAt f z := by
|
||||
exact h₁f (sorryAx ℂ true) trivial
|
||||
exact ∑ᶠ z ∈ Metric.ball (0 : ℂ) r, (h₁f z trivial).order
|
||||
let A := h₁f.mono (by tauto : Metric.closedBall (0 : ℂ) r ⊆ ⊤)
|
||||
exact ∑ᶠ z, (A.order z).toNat
|
||||
|
||||
noncomputable def integratedCounting : ℝ → ℝ := by
|
||||
intro r
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
import Mathlib.Analysis.Complex.CauchyIntegral
|
||||
import Mathlib.Analysis.Analytic.IsolatedZeros
|
||||
import Nevanlinna.analyticOnNhd_zeroSet
|
||||
import Nevanlinna.analyticOn_zeroSet
|
||||
import Nevanlinna.harmonicAt_examples
|
||||
import Nevanlinna.harmonicAt_meanValue
|
||||
import Nevanlinna.specialFunctions_CircleIntegral_affine
|
||||
|
|
@ -11,7 +11,7 @@ open Real
|
|||
|
||||
theorem jensen_case_R_eq_one
|
||||
(f : ℂ → ℂ)
|
||||
(h₁f : AnalyticOnNhd ℂ f (Metric.closedBall 0 1))
|
||||
(h₁f : AnalyticOn ℂ f (Metric.closedBall 0 1))
|
||||
(h₂f : f 0 ≠ 0) :
|
||||
log ‖f 0‖ = -∑ᶠ s, (h₁f.order s).toNat * log (‖s.1‖⁻¹) + (2 * π)⁻¹ * ∫ (x : ℝ) in (0)..(2 * π), log ‖f (circleMap 0 1 x)‖ := by
|
||||
|
||||
|
|
@ -24,7 +24,7 @@ theorem jensen_case_R_eq_one
|
|||
have h'₂f : ∃ u ∈ (Metric.closedBall (0 : ℂ) 1), f u ≠ 0 := by
|
||||
use 0; simp; exact h₂f
|
||||
|
||||
obtain ⟨F, h₁F, h₂F, h₃F⟩ := AnalyticOnNhdCompact.eliminateZeros₂ h₁U h₂U h₁f h'₂f
|
||||
obtain ⟨F, h₁F, h₂F, h₃F⟩ := AnalyticOnCompact.eliminateZeros₂ h₁U h₂U h₁f h'₂f
|
||||
|
||||
have h'₁F : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt F z := by
|
||||
intro z h₁z
|
||||
|
|
@ -259,9 +259,9 @@ theorem jensen_case_R_eq_one
|
|||
intro x ⟨h₁x, _⟩
|
||||
simp
|
||||
|
||||
dsimp [AnalyticOnNhd.order] at h₁x
|
||||
dsimp [AnalyticOn.order] at h₁x
|
||||
simp only [Function.mem_support, ne_eq, Nat.cast_eq_zero, not_or] at h₁x
|
||||
exact AnalyticAt.supp_order_toNat (AnalyticOnNhd.order.proof_1 h₁f x) h₁x
|
||||
exact AnalyticAt.supp_order_toNat (AnalyticOn.order.proof_1 h₁f x) h₁x
|
||||
|
||||
--
|
||||
intro x hx
|
||||
|
|
@ -297,7 +297,7 @@ theorem jensen
|
|||
{R : ℝ}
|
||||
(hR : 0 < R)
|
||||
(f : ℂ → ℂ)
|
||||
(h₁f : AnalyticOnNhd ℂ f (Metric.closedBall 0 R))
|
||||
(h₁f : AnalyticOn ℂ f (Metric.closedBall 0 R))
|
||||
(h₂f : f 0 ≠ 0) :
|
||||
log ‖f 0‖ = -∑ᶠ s, (h₁f.order s).toNat * log (R * ‖s.1‖⁻¹) + (2 * π)⁻¹ * ∫ (x : ℝ) in (0)..(2 * π), log ‖f (circleMap 0 R x)‖ := by
|
||||
|
||||
|
|
@ -327,8 +327,8 @@ theorem jensen
|
|||
|
||||
let F := f ∘ ℓ
|
||||
|
||||
have h₁F : AnalyticOnNhd ℂ F (Metric.closedBall 0 1) := by
|
||||
apply AnalyticOnNhd.comp (t := Metric.closedBall 0 R)
|
||||
have h₁F : AnalyticOn ℂ F (Metric.closedBall 0 1) := by
|
||||
apply AnalyticOn.comp (t := Metric.closedBall 0 R)
|
||||
exact h₁f
|
||||
intro x _
|
||||
apply ℓ.toContinuousLinearMap.analyticAt x
|
||||
|
|
@ -430,7 +430,7 @@ theorem jensen
|
|||
left
|
||||
congr 1
|
||||
|
||||
dsimp [AnalyticOnNhd.order]
|
||||
dsimp [AnalyticOn.order]
|
||||
rw [← AnalyticAt.order_comp_CLE ℓ]
|
||||
|
||||
--
|
||||
|
|
|
|||
|
|
@ -277,7 +277,7 @@ theorem harmonic_is_realOfHolomorphic
|
|||
|
||||
intro x hx
|
||||
rw [fderivWithin_eq_fderiv, fderivWithin_eq_fderiv]
|
||||
rw [fderiv_comp]
|
||||
rw [fderiv.comp]
|
||||
simp
|
||||
apply ContinuousLinearMap.ext
|
||||
intro w
|
||||
|
|
|
|||
|
|
@ -666,7 +666,7 @@ theorem primitive_additivity'
|
|||
dsimp [ε']; simp
|
||||
have : |ε| = ε := by apply abs_of_pos h₁ε
|
||||
rw [this]
|
||||
apply (inv_mul_lt_iff₀ zero_lt_two).mpr
|
||||
apply (inv_mul_lt_iff zero_lt_two).mpr
|
||||
linarith
|
||||
have h₁ε' : 0 < ε' := by
|
||||
apply mul_pos _ h₁ε
|
||||
|
|
|
|||
|
|
@ -3,7 +3,7 @@ import Mathlib.Analysis.Analytic.Meromorphic
|
|||
import Mathlib.Topology.ContinuousOn
|
||||
import Mathlib.Analysis.Analytic.IsolatedZeros
|
||||
import Nevanlinna.holomorphic
|
||||
import Nevanlinna.analyticOnNhd_zeroSet
|
||||
import Nevanlinna.analyticOn_zeroSet
|
||||
|
||||
|
||||
noncomputable def zeroDivisor
|
||||
|
|
@ -134,7 +134,7 @@ theorem topOnPreconnected
|
|||
{f : ℂ → ℂ}
|
||||
{U : Set ℂ}
|
||||
(hU : IsPreconnected U)
|
||||
(h₁f : AnalyticOnNhd ℂ f U)
|
||||
(h₁f : AnalyticOn ℂ f U)
|
||||
(h₂f : ∃ z ∈ U, f z ≠ 0) :
|
||||
∀ (hz : z ∈ U), (h₁f z hz).order ≠ ⊤ := by
|
||||
|
||||
|
|
@ -143,7 +143,7 @@ theorem topOnPreconnected
|
|||
obtain ⟨z', hz'⟩ := H
|
||||
rw [AnalyticAt.order_eq_top_iff] at hz'
|
||||
rw [← AnalyticAt.frequently_zero_iff_eventually_zero (h₁f z z')] at hz'
|
||||
have A := AnalyticOnNhd.eqOn_zero_of_preconnected_of_frequently_eq_zero h₁f hU z' hz'
|
||||
have A := AnalyticOn.eqOn_zero_of_preconnected_of_frequently_eq_zero h₁f hU z' hz'
|
||||
tauto
|
||||
|
||||
|
||||
|
|
@ -151,7 +151,7 @@ theorem supportZeroSet
|
|||
{f : ℂ → ℂ}
|
||||
{U : Set ℂ}
|
||||
(hU : IsPreconnected U)
|
||||
(h₁f : AnalyticOnNhd ℂ f U)
|
||||
(h₁f : AnalyticOn ℂ f U)
|
||||
(h₂f : ∃ z ∈ U, f z ≠ 0) :
|
||||
U ∩ Function.support (zeroDivisor f) = U ∩ f⁻¹' {0} := by
|
||||
|
||||
|
|
@ -180,7 +180,7 @@ theorem supportZeroSet
|
|||
refine Eq.symm (ENat.coe_toNat ?h.mpr.right.right.right.a)
|
||||
exact topOnPreconnected hU h₁f h₂f h₁x
|
||||
|
||||
/-
|
||||
|
||||
theorem discreteZeros
|
||||
{f : ℂ → ℂ} :
|
||||
DiscreteTopology (Function.support (zeroDivisor f)) := by
|
||||
|
|
@ -254,13 +254,13 @@ theorem discreteZeros
|
|||
simp [this] at F
|
||||
ext
|
||||
rwa [sub_eq_zero] at F
|
||||
-/
|
||||
|
||||
|
||||
theorem zeroDivisor_finiteOnCompact
|
||||
{f : ℂ → ℂ}
|
||||
{U : Set ℂ}
|
||||
(hU : IsPreconnected U)
|
||||
(h₁f : AnalyticOnNhd ℂ f U)
|
||||
(h₁f : AnalyticOn ℂ f U)
|
||||
(h₂f : ∃ z ∈ U, f z ≠ 0) -- not needed!
|
||||
(h₂U : IsCompact U) :
|
||||
Set.Finite (U ∩ Function.support (zeroDivisor f)) := by
|
||||
|
|
@ -289,7 +289,7 @@ noncomputable def zeroDivisorDegree
|
|||
{U : Set ℂ}
|
||||
(h₁U : IsPreconnected U) -- not needed!
|
||||
(h₂U : IsCompact U)
|
||||
(h₁f : AnalyticOnNhd ℂ f U)
|
||||
(h₁f : AnalyticOn ℂ f U)
|
||||
(h₂f : ∃ z ∈ U, f z ≠ 0) : -- not needed!
|
||||
ℕ := (zeroDivisor_finiteOnCompact h₁U h₁f h₂f h₂U).toFinset.card
|
||||
|
||||
|
|
@ -299,7 +299,7 @@ lemma zeroDivisorDegreeZero
|
|||
{U : Set ℂ}
|
||||
(h₁U : IsPreconnected U) -- not needed!
|
||||
(h₂U : IsCompact U)
|
||||
(h₁f : AnalyticOnNhd ℂ f U)
|
||||
(h₁f : AnalyticOn ℂ f U)
|
||||
(h₂f : ∃ z ∈ U, f z ≠ 0) : -- not needed!
|
||||
0 = zeroDivisorDegree h₁U h₂U h₁f h₂f ↔ U ∩ (zeroDivisor f).support = ∅ := by
|
||||
sorry
|
||||
|
|
@ -309,9 +309,9 @@ lemma eliminatingZeros₀
|
|||
{U : Set ℂ}
|
||||
(h₁U : IsPreconnected U)
|
||||
(h₂U : IsCompact U) :
|
||||
∀ n : ℕ, ∀ f : ℂ → ℂ, (h₁f : AnalyticOnNhd ℂ f U) → (h₂f : ∃ z ∈ U, f z ≠ 0) →
|
||||
∀ n : ℕ, ∀ f : ℂ → ℂ, (h₁f : AnalyticOn ℂ f U) → (h₂f : ∃ z ∈ U, f z ≠ 0) →
|
||||
(n = zeroDivisorDegree h₁U h₂U h₁f h₂f) →
|
||||
∃ F : ℂ → ℂ, (AnalyticOnNhd ℂ F U) ∧ (f = F * ∏ᶠ a ∈ (U ∩ (zeroDivisor f).support), fun z ↦ (z - a) ^ (zeroDivisor f a)) := by
|
||||
∃ F : ℂ → ℂ, (AnalyticOn ℂ F U) ∧ (f = F * ∏ᶠ a ∈ (U ∩ (zeroDivisor f).support), fun z ↦ (z - a) ^ (zeroDivisor f a)) := by
|
||||
|
||||
intro n
|
||||
induction' n with n ih
|
||||
|
|
@ -340,7 +340,7 @@ lemma eliminatingZeros₀
|
|||
|
||||
|
||||
|
||||
let A := AnalyticOnNhd.order_eq_nat_iff h₁f hz₀.1 (zeroDivisor f z₀)
|
||||
let A := AnalyticOn.order_eq_nat_iff h₁f hz₀.1 (zeroDivisor f z₀)
|
||||
let B := zeroDivisor_eq_ord_AtZeroDivisorSupport hz₀.2
|
||||
let B := zeroDivisor_eq_ord_AtZeroDivisorSupport' hz₀.2
|
||||
rw [eq_comm] at B
|
||||
|
|
|
|||
|
|
@ -1,7 +1,5 @@
|
|||
import Mathlib.Analysis.Analytic.Meromorphic
|
||||
import Mathlib.Analysis.Calculus.ContDiff.Basic
|
||||
import Mathlib.Analysis.Calculus.FDeriv.Add
|
||||
import Nevanlinna.analyticAt
|
||||
|
||||
variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
|
||||
variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
|
||||
|
|
@ -35,62 +33,3 @@ theorem ContDiff.const_smul' {f : E → F} (c : R) (hf : ContDiff 𝕜 n f) :
|
|||
have : c • f = fun x ↦ c • f x := rfl
|
||||
rw [this]
|
||||
exact ContDiff.const_smul c hf
|
||||
|
||||
|
||||
|
||||
open Topology Filter
|
||||
|
||||
lemma Mnhds
|
||||
{α : Type}
|
||||
{f g : ℂ → α}
|
||||
{z₀ : ℂ}
|
||||
(h₁ : f =ᶠ[𝓝[≠] z₀] g)
|
||||
(h₂ : f z₀ = g z₀) :
|
||||
f =ᶠ[𝓝 z₀] g := by
|
||||
apply eventually_nhds_iff.2
|
||||
obtain ⟨t, h₁t, h₂t⟩ := eventually_nhds_iff.1 (eventually_nhdsWithin_iff.1 h₁)
|
||||
use t
|
||||
constructor
|
||||
· intro y hy
|
||||
by_cases h₂y : y ∈ ({z₀}ᶜ : Set ℂ)
|
||||
· exact h₁t y hy h₂y
|
||||
· simp at h₂y
|
||||
rwa [h₂y]
|
||||
· exact h₂t
|
||||
|
||||
-- unclear where this should go
|
||||
|
||||
lemma WithTopCoe
|
||||
{n : WithTop ℕ} :
|
||||
WithTop.map (Nat.cast : ℕ → ℤ) n = 0 → n = 0 := by
|
||||
rcases n with h|h
|
||||
· intro h
|
||||
contradiction
|
||||
· intro h₁
|
||||
simp only [WithTop.map, Option.map] at h₁
|
||||
have : (h : ℤ) = 0 := by
|
||||
exact WithTop.coe_eq_zero.mp h₁
|
||||
have : h = 0 := by
|
||||
exact Int.ofNat_eq_zero.mp this
|
||||
rw [this]
|
||||
rfl
|
||||
|
||||
|
||||
|
||||
|
||||
lemma rwx
|
||||
{a b : WithTop ℤ}
|
||||
(ha : a ≠ ⊤)
|
||||
(hb : b ≠ ⊤) :
|
||||
a + b ≠ ⊤ := by
|
||||
simp; tauto
|
||||
|
||||
lemma untop_add
|
||||
{a b : WithTop ℤ}
|
||||
(ha : a ≠ ⊤)
|
||||
(hb : b ≠ ⊤) :
|
||||
(a + b).untop (rwx ha hb) = a.untop ha + (b.untop hb) := by
|
||||
rw [WithTop.untop_eq_iff]
|
||||
rw [WithTop.coe_add]
|
||||
rw [WithTop.coe_untop]
|
||||
rw [WithTop.coe_untop]
|
||||
|
|
|
|||
|
|
@ -1,150 +0,0 @@
|
|||
import Mathlib.Analysis.Analytic.Meromorphic
|
||||
import Nevanlinna.analyticAt
|
||||
import Nevanlinna.divisor
|
||||
|
||||
|
||||
open scoped Interval Topology
|
||||
open Real Filter MeasureTheory intervalIntegral
|
||||
|
||||
|
||||
theorem meromorphicAt_congr
|
||||
{𝕜 : Type u_1} [NontriviallyNormedField 𝕜]
|
||||
{E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
|
||||
{f : 𝕜 → E} {g : 𝕜 → E} {x : 𝕜}
|
||||
(h : f =ᶠ[nhdsWithin x {x}ᶜ] g) : MeromorphicAt f x ↔ MeromorphicAt g x :=
|
||||
⟨fun hf ↦ hf.congr h, fun hg ↦ hg.congr h.symm⟩
|
||||
|
||||
|
||||
theorem meromorphicAt_congr'
|
||||
{𝕜 : Type u_1} [NontriviallyNormedField 𝕜]
|
||||
{E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
|
||||
{f : 𝕜 → E} {g : 𝕜 → E} {x : 𝕜}
|
||||
(h : f =ᶠ[nhds x] g) : MeromorphicAt f x ↔ MeromorphicAt g x :=
|
||||
meromorphicAt_congr (Filter.EventuallyEq.filter_mono h nhdsWithin_le_nhds)
|
||||
|
||||
|
||||
theorem MeromorphicAt.eventually_eq_zero_or_eventually_ne_zero
|
||||
{f : ℂ → ℂ}
|
||||
{z₀ : ℂ}
|
||||
(hf : MeromorphicAt f z₀) :
|
||||
(∀ᶠ (z : ℂ) in nhdsWithin z₀ {z₀}ᶜ, f z = 0) ∨ ∀ᶠ (z : ℂ) in nhdsWithin z₀ {z₀}ᶜ, f z ≠ 0 := by
|
||||
|
||||
obtain ⟨n, h⟩ := hf
|
||||
let A := h.eventually_eq_zero_or_eventually_ne_zero
|
||||
|
||||
rw [eventually_nhdsWithin_iff]
|
||||
rw [eventually_nhds_iff]
|
||||
rcases A with h₁|h₂
|
||||
· rw [eventually_nhds_iff] at h₁
|
||||
obtain ⟨N, h₁N, h₂N, h₃N⟩ := h₁
|
||||
left
|
||||
use N
|
||||
constructor
|
||||
· intro y h₁y h₂y
|
||||
let A := h₁N y h₁y
|
||||
simp at A
|
||||
rcases A with h₃|h₄
|
||||
· let B := h₃.1
|
||||
simp at h₂y
|
||||
let C := sub_eq_zero.1 B
|
||||
tauto
|
||||
· assumption
|
||||
· constructor
|
||||
· exact h₂N
|
||||
· exact h₃N
|
||||
· right
|
||||
rw [eventually_nhdsWithin_iff]
|
||||
rw [eventually_nhds_iff]
|
||||
rw [eventually_nhdsWithin_iff] at h₂
|
||||
rw [eventually_nhds_iff] at h₂
|
||||
obtain ⟨N, h₁N, h₂N, h₃N⟩ := h₂
|
||||
use N
|
||||
constructor
|
||||
· intro y h₁y h₂y
|
||||
by_contra h
|
||||
let A := h₁N y h₁y h₂y
|
||||
rw [h] at A
|
||||
simp at A
|
||||
· constructor
|
||||
· exact h₂N
|
||||
· exact h₃N
|
||||
|
||||
|
||||
theorem MeromorphicAt.order_congr
|
||||
{f₁ f₂ : ℂ → ℂ}
|
||||
{z₀ : ℂ}
|
||||
(hf₁ : MeromorphicAt f₁ z₀)
|
||||
(h : f₁ =ᶠ[𝓝[≠] z₀] f₂):
|
||||
hf₁.order = (hf₁.congr h).order := by
|
||||
by_cases hord : hf₁.order = ⊤
|
||||
· rw [hord, eq_comm]
|
||||
rw [hf₁.order_eq_top_iff] at hord
|
||||
rw [(hf₁.congr h).order_eq_top_iff]
|
||||
exact EventuallyEq.rw hord (fun x => Eq (f₂ x)) (_root_.id (EventuallyEq.symm h))
|
||||
· obtain ⟨n, hn : hf₁.order = n⟩ := Option.ne_none_iff_exists'.mp hord
|
||||
obtain ⟨g, h₁g, h₂g, h₃g⟩ := (hf₁.order_eq_int_iff n).1 hn
|
||||
rw [hn, eq_comm, (hf₁.congr h).order_eq_int_iff]
|
||||
use g
|
||||
constructor
|
||||
· assumption
|
||||
· constructor
|
||||
· assumption
|
||||
· exact EventuallyEq.rw h₃g (fun x => Eq (f₂ x)) (_root_.id (EventuallyEq.symm h))
|
||||
|
||||
|
||||
theorem MeromorphicAt.order_mul
|
||||
{f₁ f₂ : ℂ → ℂ}
|
||||
{z₀ : ℂ}
|
||||
(hf₁ : MeromorphicAt f₁ z₀)
|
||||
(hf₂ : MeromorphicAt f₂ z₀) :
|
||||
(hf₁.mul hf₂).order = hf₁.order + hf₂.order := by
|
||||
by_cases h₂f₁ : hf₁.order = ⊤
|
||||
· simp [h₂f₁]
|
||||
rw [hf₁.order_eq_top_iff, eventually_nhdsWithin_iff, eventually_nhds_iff] at h₂f₁
|
||||
rw [(hf₁.mul hf₂).order_eq_top_iff, eventually_nhdsWithin_iff, eventually_nhds_iff]
|
||||
obtain ⟨t, h₁t, h₂t, h₃t⟩ := h₂f₁
|
||||
use t
|
||||
constructor
|
||||
· intro y h₁y h₂y
|
||||
simp; left
|
||||
rw [h₁t y h₁y h₂y]
|
||||
· exact ⟨h₂t, h₃t⟩
|
||||
· by_cases h₂f₂ : hf₂.order = ⊤
|
||||
· simp [h₂f₂]
|
||||
rw [hf₂.order_eq_top_iff, eventually_nhdsWithin_iff, eventually_nhds_iff] at h₂f₂
|
||||
rw [(hf₁.mul hf₂).order_eq_top_iff, eventually_nhdsWithin_iff, eventually_nhds_iff]
|
||||
obtain ⟨t, h₁t, h₂t, h₃t⟩ := h₂f₂
|
||||
use t
|
||||
constructor
|
||||
· intro y h₁y h₂y
|
||||
simp; right
|
||||
rw [h₁t y h₁y h₂y]
|
||||
· exact ⟨h₂t, h₃t⟩
|
||||
· have h₃f₁ := Eq.symm (WithTop.coe_untop hf₁.order h₂f₁)
|
||||
have h₃f₂ := Eq.symm (WithTop.coe_untop hf₂.order h₂f₂)
|
||||
obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (hf₁.order_eq_int_iff (hf₁.order.untop h₂f₁)).1 h₃f₁
|
||||
obtain ⟨g₂, h₁g₂, h₂g₂, h₃g₂⟩ := (hf₂.order_eq_int_iff (hf₂.order.untop h₂f₂)).1 h₃f₂
|
||||
rw [h₃f₁, h₃f₂, ← WithTop.coe_add]
|
||||
rw [MeromorphicAt.order_eq_int_iff]
|
||||
use g₁ * g₂
|
||||
constructor
|
||||
· exact AnalyticAt.mul h₁g₁ h₁g₂
|
||||
· constructor
|
||||
· simp; tauto
|
||||
· obtain ⟨t₁, h₁t₁, h₂t₁, h₃t₁⟩ := eventually_nhds_iff.1 (eventually_nhdsWithin_iff.1 h₃g₁)
|
||||
obtain ⟨t₂, h₁t₂, h₂t₂, h₃t₂⟩ := eventually_nhds_iff.1 (eventually_nhdsWithin_iff.1 h₃g₂)
|
||||
rw [eventually_nhdsWithin_iff, eventually_nhds_iff]
|
||||
use t₁ ∩ t₂
|
||||
constructor
|
||||
· intro y h₁y h₂y
|
||||
simp
|
||||
rw [h₁t₁ y h₁y.1 h₂y, h₁t₂ y h₁y.2 h₂y]
|
||||
simp
|
||||
rw [zpow_add' (by left; exact sub_ne_zero_of_ne h₂y)]
|
||||
group
|
||||
· constructor
|
||||
· exact IsOpen.inter h₂t₁ h₂t₂
|
||||
· exact Set.mem_inter h₃t₁ h₃t₂
|
||||
|
||||
|
||||
-- might want theorem MeromorphicAt.order_zpow
|
||||
|
|
@ -1,131 +0,0 @@
|
|||
import Mathlib.Analysis.Analytic.Meromorphic
|
||||
import Nevanlinna.analyticAt
|
||||
import Nevanlinna.divisor
|
||||
import Nevanlinna.meromorphicAt
|
||||
import Nevanlinna.meromorphicOn_divisor
|
||||
import Nevanlinna.stronglyMeromorphicOn
|
||||
import Nevanlinna.mathlibAddOn
|
||||
|
||||
open scoped Interval Topology
|
||||
open Real Filter MeasureTheory intervalIntegral
|
||||
|
||||
theorem MeromorphicOn.open_of_order_eq_top
|
||||
{f : ℂ → ℂ}
|
||||
{U : Set ℂ}
|
||||
(h₁f : MeromorphicOn f U) :
|
||||
IsOpen { u : U | (h₁f u.1 u.2).order = ⊤ } := by
|
||||
|
||||
apply isOpen_iff_forall_mem_open.mpr
|
||||
intro z hz
|
||||
simp at hz
|
||||
|
||||
have h₁z := hz
|
||||
rw [MeromorphicAt.order_eq_top_iff] at hz
|
||||
rw [eventually_nhdsWithin_iff] at hz
|
||||
rw [eventually_nhds_iff] at hz
|
||||
obtain ⟨t', h₁t', h₂t', h₃t'⟩ := hz
|
||||
let t : Set U := Subtype.val ⁻¹' t'
|
||||
use t
|
||||
constructor
|
||||
· intro w hw
|
||||
simp
|
||||
by_cases h₁w : w = z
|
||||
· rwa [h₁w]
|
||||
· --
|
||||
rw [MeromorphicAt.order_eq_top_iff]
|
||||
rw [eventually_nhdsWithin_iff]
|
||||
rw [eventually_nhds_iff]
|
||||
use t' \ {z.1}
|
||||
constructor
|
||||
· intro y h₁y h₂y
|
||||
apply h₁t'
|
||||
exact Set.mem_of_mem_diff h₁y
|
||||
exact Set.mem_of_mem_inter_right h₁y
|
||||
· constructor
|
||||
· apply IsOpen.sdiff h₂t'
|
||||
exact isClosed_singleton
|
||||
· rw [Set.mem_diff]
|
||||
constructor
|
||||
· exact hw
|
||||
· simp
|
||||
exact Subtype.coe_ne_coe.mpr h₁w
|
||||
|
||||
· constructor
|
||||
· exact isOpen_induced h₂t'
|
||||
· exact h₃t'
|
||||
|
||||
|
||||
theorem MeromorphicOn.open_of_order_neq_top
|
||||
{f : ℂ → ℂ}
|
||||
{U : Set ℂ}
|
||||
(h₁f : MeromorphicOn f U) :
|
||||
IsOpen { u : U | (h₁f u.1 u.2).order ≠ ⊤ } := by
|
||||
|
||||
apply isOpen_iff_forall_mem_open.mpr
|
||||
intro z hz
|
||||
simp at hz
|
||||
|
||||
let A := (h₁f z.1 z.2).eventually_eq_zero_or_eventually_ne_zero
|
||||
rcases A with h|h
|
||||
· rw [← (h₁f z.1 z.2).order_eq_top_iff] at h
|
||||
tauto
|
||||
· let A := (h₁f z.1 z.2).eventually_analyticAt
|
||||
let B := Filter.Eventually.and h A
|
||||
rw [eventually_nhdsWithin_iff] at B
|
||||
rw [eventually_nhds_iff] at B
|
||||
obtain ⟨t', h₁t', h₂t', h₃t'⟩ := B
|
||||
let t : Set U := Subtype.val ⁻¹' t'
|
||||
use t
|
||||
constructor
|
||||
· intro w hw
|
||||
simp
|
||||
by_cases h₁w : w = z
|
||||
· rwa [h₁w]
|
||||
· let B := h₁t' w hw
|
||||
simp at B
|
||||
have : (w : ℂ) ≠ (z : ℂ) := by exact Subtype.coe_ne_coe.mpr h₁w
|
||||
let C := B this
|
||||
let D := C.2.order_eq_zero_iff.2 C.1
|
||||
rw [C.2.meromorphicAt_order, D]
|
||||
simp
|
||||
· constructor
|
||||
· exact isOpen_induced h₂t'
|
||||
· exact h₃t'
|
||||
|
||||
|
||||
theorem MeromorphicOn.clopen_of_order_eq_top
|
||||
{f : ℂ → ℂ}
|
||||
{U : Set ℂ}
|
||||
(h₁f : MeromorphicOn f U) :
|
||||
IsClopen { u : U | (h₁f u.1 u.2).order = ⊤ } := by
|
||||
|
||||
constructor
|
||||
· rw [← isOpen_compl_iff]
|
||||
exact open_of_order_neq_top h₁f
|
||||
· exact open_of_order_eq_top h₁f
|
||||
|
||||
|
||||
theorem MeromorphicOn.order_ne_top
|
||||
{U : Set ℂ}
|
||||
(hU : IsConnected U)
|
||||
(h₁f : StronglyMeromorphicOn f U)
|
||||
(h₂f : ∃ u : U, f u ≠ 0) :
|
||||
∀ u : U, (h₁f u u.2).meromorphicAt.order ≠ ⊤ := by
|
||||
|
||||
let A := h₁f.meromorphicOn.clopen_of_order_eq_top
|
||||
have : PreconnectedSpace U := by
|
||||
apply isPreconnected_iff_preconnectedSpace.mp
|
||||
exact IsConnected.isPreconnected hU
|
||||
rw [isClopen_iff] at A
|
||||
rcases A with h|h
|
||||
· intro u
|
||||
have : u ∉ (∅ : Set U) := by exact fun a => a
|
||||
rw [← h] at this
|
||||
simp at this
|
||||
tauto
|
||||
· obtain ⟨u, hu⟩ := h₂f
|
||||
have : u ∈ (Set.univ : Set U) := by trivial
|
||||
rw [← h] at this
|
||||
simp at this
|
||||
rw [(h₁f u u.2).order_eq_zero_iff.2 hu] at this
|
||||
tauto
|
||||
|
|
@ -1,144 +0,0 @@
|
|||
import Mathlib.Analysis.Analytic.Meromorphic
|
||||
import Nevanlinna.analyticAt
|
||||
import Nevanlinna.divisor
|
||||
import Nevanlinna.meromorphicAt
|
||||
|
||||
|
||||
open scoped Interval Topology
|
||||
open Real Filter MeasureTheory intervalIntegral
|
||||
|
||||
|
||||
noncomputable def MeromorphicOn.divisor
|
||||
{f : ℂ → ℂ}
|
||||
{U : Set ℂ}
|
||||
(hf : MeromorphicOn f U) :
|
||||
Divisor U where
|
||||
|
||||
toFun := by
|
||||
intro z
|
||||
if hz : z ∈ U then
|
||||
exact ((hf z hz).order.untop' 0 : ℤ)
|
||||
else
|
||||
exact 0
|
||||
|
||||
supportInU := by
|
||||
intro z hz
|
||||
simp at hz
|
||||
by_contra h₂z
|
||||
simp [h₂z] at hz
|
||||
|
||||
locallyFiniteInU := by
|
||||
intro z hz
|
||||
|
||||
apply eventually_nhdsWithin_iff.2
|
||||
rw [eventually_nhds_iff]
|
||||
|
||||
rcases MeromorphicAt.eventually_eq_zero_or_eventually_ne_zero (hf z hz) with h|h
|
||||
· rw [eventually_nhdsWithin_iff] at h
|
||||
rw [eventually_nhds_iff] at h
|
||||
obtain ⟨N, h₁N, h₂N, h₃N⟩ := h
|
||||
use N
|
||||
constructor
|
||||
· intro y h₁y h₂y
|
||||
by_cases h₃y : y ∈ U
|
||||
· simp [h₃y]
|
||||
right
|
||||
rw [MeromorphicAt.order_eq_top_iff (hf y h₃y)]
|
||||
rw [eventually_nhdsWithin_iff]
|
||||
rw [eventually_nhds_iff]
|
||||
use N ∩ {z}ᶜ
|
||||
constructor
|
||||
· intro x h₁x _
|
||||
exact h₁N x h₁x.1 h₁x.2
|
||||
· constructor
|
||||
· exact IsOpen.inter h₂N isOpen_compl_singleton
|
||||
· exact Set.mem_inter h₁y h₂y
|
||||
· simp [h₃y]
|
||||
· tauto
|
||||
|
||||
· let A := (hf z hz).eventually_analyticAt
|
||||
let B := Filter.eventually_and.2 ⟨h, A⟩
|
||||
rw [eventually_nhdsWithin_iff, eventually_nhds_iff] at B
|
||||
obtain ⟨N, h₁N, h₂N, h₃N⟩ := B
|
||||
use N
|
||||
constructor
|
||||
· intro y h₁y h₂y
|
||||
by_cases h₃y : y ∈ U
|
||||
· simp [h₃y]
|
||||
left
|
||||
rw [(h₁N y h₁y h₂y).2.meromorphicAt_order]
|
||||
let D := (h₁N y h₁y h₂y).2.order_eq_zero_iff.2
|
||||
let C := (h₁N y h₁y h₂y).1
|
||||
let E := D C
|
||||
rw [E]
|
||||
simp
|
||||
· simp [h₃y]
|
||||
· tauto
|
||||
|
||||
|
||||
theorem MeromorphicOn.divisor_def₁
|
||||
{f : ℂ → ℂ}
|
||||
{U : Set ℂ}
|
||||
{z : ℂ}
|
||||
(hf : MeromorphicOn f U)
|
||||
(hz : z ∈ U) :
|
||||
hf.divisor z = ((hf z hz).order.untop' 0 : ℤ) := by
|
||||
unfold MeromorphicOn.divisor
|
||||
simp [hz]
|
||||
|
||||
|
||||
theorem MeromorphicOn.divisor_def₂
|
||||
{f : ℂ → ℂ}
|
||||
{U : Set ℂ}
|
||||
{z : ℂ}
|
||||
(hf : MeromorphicOn f U)
|
||||
(hz : z ∈ U)
|
||||
(h₂f : (hf z hz).order ≠ ⊤) :
|
||||
hf.divisor z = (hf z hz).order.untop h₂f := by
|
||||
unfold MeromorphicOn.divisor
|
||||
simp [hz]
|
||||
rw [WithTop.untop'_eq_iff]
|
||||
left
|
||||
exact Eq.symm (WithTop.coe_untop (hf z hz).order h₂f)
|
||||
|
||||
|
||||
theorem MeromorphicOn.divisor_mul₀
|
||||
{f₁ f₂ : ℂ → ℂ}
|
||||
{U : Set ℂ}
|
||||
{z : ℂ}
|
||||
(hz : z ∈ U)
|
||||
(h₁f₁ : MeromorphicOn f₁ U)
|
||||
(h₂f₁ : (h₁f₁ z hz).order ≠ ⊤)
|
||||
(h₁f₂ : MeromorphicOn f₂ U)
|
||||
(h₂f₂ : (h₁f₂ z hz).order ≠ ⊤) :
|
||||
(h₁f₁.mul h₁f₂).divisor.toFun z = h₁f₁.divisor.toFun z + h₁f₂.divisor.toFun z := by
|
||||
by_cases h₁z : z ∈ U
|
||||
· rw [MeromorphicOn.divisor_def₂ h₁f₁ hz h₂f₁]
|
||||
rw [MeromorphicOn.divisor_def₂ h₁f₂ hz h₂f₂]
|
||||
have B : ((h₁f₁.mul h₁f₂) z hz).order ≠ ⊤ := by
|
||||
rw [MeromorphicAt.order_mul (h₁f₁ z hz) (h₁f₂ z hz)]
|
||||
simp; tauto
|
||||
rw [MeromorphicOn.divisor_def₂ (h₁f₁.mul h₁f₂) hz B]
|
||||
simp_rw [MeromorphicAt.order_mul (h₁f₁ z hz) (h₁f₂ z hz)]
|
||||
rw [untop_add]
|
||||
· unfold MeromorphicOn.divisor
|
||||
simp [h₁z]
|
||||
|
||||
|
||||
theorem MeromorphicOn.divisor_mul
|
||||
{f₁ f₂ : ℂ → ℂ}
|
||||
{U : Set ℂ}
|
||||
(h₁f₁ : MeromorphicOn f₁ U)
|
||||
(h₂f₁ : ∀ z, (hz : z ∈ U) → (h₁f₁ z hz).order ≠ ⊤)
|
||||
(h₁f₂ : MeromorphicOn f₂ U)
|
||||
(h₂f₂ : ∀ z, (hz : z ∈ U) → (h₁f₂ z hz).order ≠ ⊤) :
|
||||
(h₁f₁.mul h₁f₂).divisor.toFun = h₁f₁.divisor.toFun + h₁f₂.divisor.toFun := by
|
||||
funext z
|
||||
by_cases hz : z ∈ U
|
||||
· rw [MeromorphicOn.divisor_mul₀ hz h₁f₁ (h₂f₁ z hz) h₁f₂ (h₂f₂ z hz)]
|
||||
simp
|
||||
· simp
|
||||
rw [Function.nmem_support.mp (fun a => hz (h₁f₁.divisor.supportInU a))]
|
||||
rw [Function.nmem_support.mp (fun a => hz (h₁f₂.divisor.supportInU a))]
|
||||
rw [Function.nmem_support.mp (fun a => hz ((h₁f₁.mul h₁f₂).divisor.supportInU a))]
|
||||
simp
|
||||
|
|
@ -202,14 +202,14 @@ theorem partialDeriv_compContLin
|
|||
left
|
||||
intro w
|
||||
left
|
||||
rw [fderiv_comp w (ContinuousLinearMap.differentiableAt l) (h w)]
|
||||
rw [fderiv.comp w (ContinuousLinearMap.differentiableAt l) (h w)]
|
||||
simp
|
||||
rfl
|
||||
|
||||
|
||||
theorem partialDeriv_compContLinAt {f : E → F} {l : F →L[𝕜] G} {v : E} {x : E} (h : DifferentiableAt 𝕜 f x) : (partialDeriv 𝕜 v (l ∘ f)) x = (l ∘ partialDeriv 𝕜 v f) x:= by
|
||||
unfold partialDeriv
|
||||
rw [fderiv_comp x (ContinuousLinearMap.differentiableAt l) h]
|
||||
rw [fderiv.comp x (ContinuousLinearMap.differentiableAt l) h]
|
||||
simp
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -24,7 +24,7 @@ lemma logsinBound : ∀ x ∈ (Set.Icc 0 1), ‖(log ∘ sin) x‖ ≤ ‖log ((
|
|||
exact zero_lt_two
|
||||
apply (Set.mem_Icc.1 hx).1
|
||||
simp
|
||||
apply mul_le_one₀
|
||||
apply mul_le_one
|
||||
rw [div_le_one pi_pos]
|
||||
exact two_le_pi
|
||||
exact (Set.mem_Icc.1 hx).1
|
||||
|
|
|
|||
|
|
@ -1,513 +0,0 @@
|
|||
import Mathlib.Analysis.Analytic.Meromorphic
|
||||
import Mathlib.Algebra.Order.AddGroupWithTop
|
||||
import Nevanlinna.analyticAt
|
||||
import Nevanlinna.mathlibAddOn
|
||||
import Nevanlinna.meromorphicAt
|
||||
|
||||
|
||||
open Topology
|
||||
|
||||
|
||||
/- Strongly MeromorphicAt -/
|
||||
def StronglyMeromorphicAt
|
||||
(f : ℂ → ℂ)
|
||||
(z₀ : ℂ) :=
|
||||
(∀ᶠ (z : ℂ) in nhds z₀, f z = 0) ∨ (∃ (n : ℤ), ∃ g : ℂ → ℂ, (AnalyticAt ℂ g z₀) ∧ (g z₀ ≠ 0) ∧ (∀ᶠ (z : ℂ) in nhds z₀, f z = (z - z₀) ^ n • g z))
|
||||
|
||||
|
||||
lemma stronglyMeromorphicAt_of_mul_analytic'
|
||||
{f g : ℂ → ℂ}
|
||||
{z₀ : ℂ}
|
||||
(h₁g : AnalyticAt ℂ g z₀)
|
||||
(h₂g : g z₀ ≠ 0) :
|
||||
StronglyMeromorphicAt f z₀ → StronglyMeromorphicAt (f * g) z₀ := by
|
||||
|
||||
intro hf
|
||||
--unfold StronglyMeromorphicAt at hf
|
||||
rcases hf with h₁f|h₁f
|
||||
· left
|
||||
rw [eventually_nhds_iff] at h₁f
|
||||
obtain ⟨t, ht⟩ := h₁f
|
||||
rw [eventually_nhds_iff]
|
||||
use t
|
||||
constructor
|
||||
· intro y hy
|
||||
simp
|
||||
left
|
||||
exact ht.1 y hy
|
||||
· exact ht.2
|
||||
· right
|
||||
obtain ⟨n, g_f, h₁g_f, h₂g_f, h₃g_f⟩ := h₁f
|
||||
use n
|
||||
use g * g_f
|
||||
constructor
|
||||
· apply AnalyticAt.mul
|
||||
exact h₁g
|
||||
exact h₁g_f
|
||||
· constructor
|
||||
· simp
|
||||
exact ⟨h₂g, h₂g_f⟩
|
||||
· rw [eventually_nhds_iff] at h₃g_f
|
||||
obtain ⟨t, ht⟩ := h₃g_f
|
||||
rw [eventually_nhds_iff]
|
||||
use t
|
||||
constructor
|
||||
· intro y hy
|
||||
simp
|
||||
rw [ht.1]
|
||||
simp
|
||||
ring
|
||||
exact hy
|
||||
· exact ht.2
|
||||
|
||||
|
||||
/- Strongly MeromorphicAt is Meromorphic -/
|
||||
theorem StronglyMeromorphicAt.meromorphicAt
|
||||
{f : ℂ → ℂ}
|
||||
{z₀ : ℂ}
|
||||
(hf : StronglyMeromorphicAt f z₀) :
|
||||
MeromorphicAt f z₀ := by
|
||||
rcases hf with h|h
|
||||
· use 0; simp
|
||||
rw [analyticAt_congr h]
|
||||
exact analyticAt_const
|
||||
· obtain ⟨n, g, h₁g, _, h₃g⟩ := h
|
||||
rw [meromorphicAt_congr' h₃g]
|
||||
apply MeromorphicAt.smul
|
||||
apply MeromorphicAt.zpow
|
||||
apply MeromorphicAt.sub
|
||||
apply MeromorphicAt.id
|
||||
apply MeromorphicAt.const
|
||||
exact AnalyticAt.meromorphicAt h₁g
|
||||
|
||||
|
||||
/- Strongly MeromorphicAt of non-negative order is analytic -/
|
||||
theorem StronglyMeromorphicAt.analytic
|
||||
{f : ℂ → ℂ}
|
||||
{z₀ : ℂ}
|
||||
(h₁f : StronglyMeromorphicAt f z₀)
|
||||
(h₂f : 0 ≤ h₁f.meromorphicAt.order):
|
||||
AnalyticAt ℂ f z₀ := by
|
||||
let h₁f' := h₁f
|
||||
rcases h₁f' with h|h
|
||||
· rw [analyticAt_congr h]
|
||||
exact analyticAt_const
|
||||
· obtain ⟨n, g, h₁g, h₂g, h₃g⟩ := h
|
||||
rw [analyticAt_congr h₃g]
|
||||
|
||||
have : h₁f.meromorphicAt.order = n := by
|
||||
rw [MeromorphicAt.order_eq_int_iff]
|
||||
use g
|
||||
constructor
|
||||
· exact h₁g
|
||||
· constructor
|
||||
· exact h₂g
|
||||
· exact Filter.EventuallyEq.filter_mono h₃g nhdsWithin_le_nhds
|
||||
rw [this] at h₂f
|
||||
apply AnalyticAt.smul
|
||||
nth_rw 1 [← Int.toNat_of_nonneg (WithTop.coe_nonneg.mp h₂f)]
|
||||
apply AnalyticAt.pow
|
||||
apply AnalyticAt.sub
|
||||
apply analyticAt_id -- Warning: want apply AnalyticAt.id
|
||||
apply analyticAt_const -- Warning: want AnalyticAt.const
|
||||
exact h₁g
|
||||
|
||||
|
||||
/- Analytic functions are strongly meromorphic -/
|
||||
theorem AnalyticAt.stronglyMeromorphicAt
|
||||
{f : ℂ → ℂ}
|
||||
{z₀ : ℂ}
|
||||
(h₁f : AnalyticAt ℂ f z₀) :
|
||||
StronglyMeromorphicAt f z₀ := by
|
||||
by_cases h₂f : h₁f.order = ⊤
|
||||
· rw [AnalyticAt.order_eq_top_iff] at h₂f
|
||||
tauto
|
||||
· have : h₁f.order ≠ ⊤ := h₂f
|
||||
rw [← ENat.coe_toNat_eq_self] at this
|
||||
rw [eq_comm, AnalyticAt.order_eq_nat_iff] at this
|
||||
right
|
||||
use h₁f.order.toNat
|
||||
obtain ⟨g, h₁g, h₂g, h₃g⟩ := this
|
||||
use g
|
||||
tauto
|
||||
|
||||
|
||||
/- Strong meromorphic depends only on germ -/
|
||||
theorem stronglyMeromorphicAt_congr
|
||||
{f g : ℂ → ℂ}
|
||||
{z₀ : ℂ}
|
||||
(hfg : f =ᶠ[𝓝 z₀] g) :
|
||||
StronglyMeromorphicAt f z₀ ↔ StronglyMeromorphicAt g z₀ := by
|
||||
unfold StronglyMeromorphicAt
|
||||
constructor
|
||||
· intro h
|
||||
rcases h with h|h
|
||||
· left
|
||||
exact Filter.EventuallyEq.rw h (fun x => Eq (g x)) (id (Filter.EventuallyEq.symm hfg))
|
||||
· obtain ⟨n, h, h₁h, h₂h, h₃h⟩ := h
|
||||
right
|
||||
use n
|
||||
use h
|
||||
constructor
|
||||
· assumption
|
||||
· constructor
|
||||
· assumption
|
||||
· apply Filter.EventuallyEq.trans hfg.symm
|
||||
assumption
|
||||
· intro h
|
||||
rcases h with h|h
|
||||
· left
|
||||
exact Filter.EventuallyEq.rw h (fun x => Eq (f x)) hfg
|
||||
· obtain ⟨n, h, h₁h, h₂h, h₃h⟩ := h
|
||||
right
|
||||
use n
|
||||
use h
|
||||
constructor
|
||||
· assumption
|
||||
· constructor
|
||||
· assumption
|
||||
· apply Filter.EventuallyEq.trans hfg
|
||||
assumption
|
||||
|
||||
/- A function is strongly meromorphic at a point iff it is strongly meromorphic
|
||||
after multiplication with a non-vanishing analytic function
|
||||
-/
|
||||
theorem stronglyMeromorphicAt_of_mul_analytic
|
||||
{f g : ℂ → ℂ}
|
||||
{z₀ : ℂ}
|
||||
(h₁g : AnalyticAt ℂ g z₀)
|
||||
(h₂g : g z₀ ≠ 0) :
|
||||
StronglyMeromorphicAt f z₀ ↔ StronglyMeromorphicAt (f * g) z₀ := by
|
||||
constructor
|
||||
· apply stronglyMeromorphicAt_of_mul_analytic' h₁g h₂g
|
||||
· intro hprod
|
||||
let g' := fun z ↦ (g z)⁻¹
|
||||
have h₁g' := h₁g.inv h₂g
|
||||
have h₂g' : g' z₀ ≠ 0 := by
|
||||
exact inv_ne_zero h₂g
|
||||
|
||||
let B := stronglyMeromorphicAt_of_mul_analytic' h₁g' h₂g' (f := f * g) hprod
|
||||
have : f =ᶠ[𝓝 z₀] f * g * fun x => (g x)⁻¹ := by
|
||||
unfold Filter.EventuallyEq
|
||||
apply Filter.eventually_iff_exists_mem.mpr
|
||||
use g⁻¹' {0}ᶜ
|
||||
constructor
|
||||
· apply ContinuousAt.preimage_mem_nhds
|
||||
exact AnalyticAt.continuousAt h₁g
|
||||
exact compl_singleton_mem_nhds_iff.mpr h₂g
|
||||
· intro y hy
|
||||
simp at hy
|
||||
simp [hy]
|
||||
rwa [stronglyMeromorphicAt_congr this]
|
||||
|
||||
|
||||
theorem StronglyMeromorphicAt.order_eq_zero_iff
|
||||
{f : ℂ → ℂ}
|
||||
{z₀ : ℂ}
|
||||
(hf : StronglyMeromorphicAt f z₀) :
|
||||
hf.meromorphicAt.order = 0 ↔ f z₀ ≠ 0 := by
|
||||
constructor
|
||||
· intro h₁f
|
||||
let A := hf.analytic (le_of_eq (id (Eq.symm h₁f)))
|
||||
apply A.order_eq_zero_iff.1
|
||||
let B := A.meromorphicAt_order
|
||||
rw [h₁f] at B
|
||||
apply WithTopCoe
|
||||
rw [eq_comm]
|
||||
exact B
|
||||
· intro h
|
||||
have hf' := hf
|
||||
rcases hf with h₁|h₁
|
||||
· have : f z₀ = 0 := by
|
||||
apply Filter.EventuallyEq.eq_of_nhds h₁
|
||||
tauto
|
||||
· obtain ⟨n, g, h₁g, h₂g, h₃g⟩ := h₁
|
||||
have : n = 0 := by
|
||||
by_contra hContra
|
||||
let A := Filter.EventuallyEq.eq_of_nhds h₃g
|
||||
have : (0 : ℂ) ^ n = 0 := by
|
||||
exact zero_zpow n hContra
|
||||
simp at A
|
||||
simp_rw [this] at A
|
||||
simp at A
|
||||
tauto
|
||||
rw [this] at h₃g
|
||||
simp at h₃g
|
||||
|
||||
have : hf'.meromorphicAt.order = 0 := by
|
||||
apply (hf'.meromorphicAt.order_eq_int_iff 0).2
|
||||
use g
|
||||
constructor
|
||||
· assumption
|
||||
· constructor
|
||||
· assumption
|
||||
· simp
|
||||
apply Filter.EventuallyEq.filter_mono h₃g
|
||||
exact nhdsWithin_le_nhds
|
||||
exact this
|
||||
|
||||
|
||||
theorem StronglyMeromorphicAt.localIdentity
|
||||
{f g : ℂ → ℂ}
|
||||
{z₀ : ℂ}
|
||||
(hf : StronglyMeromorphicAt f z₀)
|
||||
(hg : StronglyMeromorphicAt g z₀) :
|
||||
f =ᶠ[𝓝[≠] z₀] g → f =ᶠ[𝓝 z₀] g := by
|
||||
|
||||
intro h
|
||||
|
||||
have t₀ : hf.meromorphicAt.order = hg.meromorphicAt.order := by
|
||||
exact hf.meromorphicAt.order_congr h
|
||||
|
||||
by_cases cs : hf.meromorphicAt.order = 0
|
||||
· rw [cs] at t₀
|
||||
have h₁f := hf.analytic (le_of_eq (id (Eq.symm cs)))
|
||||
have h₁g := hg.analytic (le_of_eq t₀)
|
||||
exact h₁f.localIdentity h₁g h
|
||||
· apply Mnhds h
|
||||
let A := cs
|
||||
rw [hf.order_eq_zero_iff] at A
|
||||
simp at A
|
||||
let B := cs
|
||||
rw [t₀] at B
|
||||
rw [hg.order_eq_zero_iff] at B
|
||||
simp at B
|
||||
rw [A, B]
|
||||
|
||||
|
||||
|
||||
/- Make strongly MeromorphicAt -/
|
||||
noncomputable def MeromorphicAt.makeStronglyMeromorphicAt
|
||||
{f : ℂ → ℂ}
|
||||
{z₀ : ℂ}
|
||||
(hf : MeromorphicAt f z₀) :
|
||||
ℂ → ℂ := by
|
||||
intro z
|
||||
by_cases z = z₀
|
||||
· by_cases h₁f : hf.order = (0 : ℤ)
|
||||
· rw [hf.order_eq_int_iff] at h₁f
|
||||
exact (Classical.choose h₁f) z₀
|
||||
· exact 0
|
||||
· exact f z
|
||||
|
||||
|
||||
lemma m₁
|
||||
{f : ℂ → ℂ}
|
||||
{z₀ : ℂ}
|
||||
(hf : MeromorphicAt f z₀) :
|
||||
∀ z ≠ z₀, f z = hf.makeStronglyMeromorphicAt z := by
|
||||
intro z hz
|
||||
unfold MeromorphicAt.makeStronglyMeromorphicAt
|
||||
simp [hz]
|
||||
|
||||
|
||||
lemma m₂
|
||||
{f : ℂ → ℂ}
|
||||
{z₀ : ℂ}
|
||||
(hf : MeromorphicAt f z₀) :
|
||||
f =ᶠ[𝓝[≠] z₀] hf.makeStronglyMeromorphicAt := by
|
||||
apply eventually_nhdsWithin_of_forall
|
||||
exact fun x a => m₁ hf x a
|
||||
|
||||
|
||||
theorem StronglyMeromorphicAt_of_makeStronglyMeromorphic
|
||||
{f : ℂ → ℂ}
|
||||
{z₀ : ℂ}
|
||||
(hf : MeromorphicAt f z₀) :
|
||||
StronglyMeromorphicAt hf.makeStronglyMeromorphicAt z₀ := by
|
||||
|
||||
by_cases h₂f : hf.order = ⊤
|
||||
· have : hf.makeStronglyMeromorphicAt =ᶠ[𝓝 z₀] 0 := by
|
||||
apply Mnhds
|
||||
· apply Filter.EventuallyEq.trans (Filter.EventuallyEq.symm (m₂ hf))
|
||||
exact (MeromorphicAt.order_eq_top_iff hf).1 h₂f
|
||||
· unfold MeromorphicAt.makeStronglyMeromorphicAt
|
||||
simp [h₂f]
|
||||
|
||||
apply AnalyticAt.stronglyMeromorphicAt
|
||||
rw [analyticAt_congr this]
|
||||
apply analyticAt_const
|
||||
· let n := hf.order.untop h₂f
|
||||
have : hf.order = n := by
|
||||
exact Eq.symm (WithTop.coe_untop hf.order h₂f)
|
||||
rw [hf.order_eq_int_iff] at this
|
||||
obtain ⟨g, h₁g, h₂g, h₃g⟩ := this
|
||||
right
|
||||
use n
|
||||
use g
|
||||
constructor
|
||||
· assumption
|
||||
· constructor
|
||||
· assumption
|
||||
· apply Mnhds
|
||||
· apply Filter.EventuallyEq.trans (Filter.EventuallyEq.symm (m₂ hf))
|
||||
exact h₃g
|
||||
· unfold MeromorphicAt.makeStronglyMeromorphicAt
|
||||
simp
|
||||
by_cases h₃f : hf.order = (0 : ℤ)
|
||||
· let h₄f := (hf.order_eq_int_iff 0).1 h₃f
|
||||
simp [h₃f]
|
||||
obtain ⟨h₁G, h₂G, h₃G⟩ := Classical.choose_spec h₄f
|
||||
simp at h₃G
|
||||
have hn : n = 0 := Eq.symm ((fun {α} {a} {b} h => (WithTop.eq_untop_iff h).mpr) h₂f (id (Eq.symm h₃f)))
|
||||
rw [hn]
|
||||
rw [hn] at h₃g; simp at h₃g
|
||||
simp
|
||||
have : g =ᶠ[𝓝 z₀] (Classical.choose h₄f) := by
|
||||
apply h₁g.localIdentity h₁G
|
||||
exact Filter.EventuallyEq.trans (Filter.EventuallyEq.symm h₃g) h₃G
|
||||
rw [Filter.EventuallyEq.eq_of_nhds this]
|
||||
· have : hf.order ≠ 0 := h₃f
|
||||
simp [this]
|
||||
left
|
||||
apply zero_zpow n
|
||||
dsimp [n]
|
||||
rwa [WithTop.untop_eq_iff h₂f]
|
||||
|
||||
|
||||
theorem StronglyMeromorphicAt.makeStronglyMeromorphic_id
|
||||
{f : ℂ → ℂ}
|
||||
{z₀ : ℂ}
|
||||
(hf : StronglyMeromorphicAt f z₀) :
|
||||
f = hf.meromorphicAt.makeStronglyMeromorphicAt := by
|
||||
|
||||
funext z
|
||||
by_cases hz : z = z₀
|
||||
· rw [hz]
|
||||
unfold MeromorphicAt.makeStronglyMeromorphicAt
|
||||
simp
|
||||
have h₀f := hf
|
||||
rcases hf with h₁f|h₁f
|
||||
· have A : f =ᶠ[𝓝[≠] z₀] 0 := by
|
||||
apply Filter.EventuallyEq.filter_mono h₁f
|
||||
exact nhdsWithin_le_nhds
|
||||
let B := (MeromorphicAt.order_eq_top_iff h₀f.meromorphicAt).2 A
|
||||
simp [B]
|
||||
exact Filter.EventuallyEq.eq_of_nhds h₁f
|
||||
· obtain ⟨n, g, h₁g, h₂g, h₃g⟩ := h₁f
|
||||
rw [Filter.EventuallyEq.eq_of_nhds h₃g]
|
||||
have : h₀f.meromorphicAt.order = n := by
|
||||
rw [MeromorphicAt.order_eq_int_iff (StronglyMeromorphicAt.meromorphicAt h₀f) n]
|
||||
use g
|
||||
constructor
|
||||
· assumption
|
||||
· constructor
|
||||
· assumption
|
||||
· exact eventually_nhdsWithin_of_eventually_nhds h₃g
|
||||
by_cases h₃f : h₀f.meromorphicAt.order = 0
|
||||
· simp [h₃f]
|
||||
have hn : n = (0 : ℤ) := by
|
||||
rw [h₃f] at this
|
||||
exact WithTop.coe_eq_zero.mp (id (Eq.symm this))
|
||||
simp_rw [hn]
|
||||
simp
|
||||
let t₀ : h₀f.meromorphicAt.order = (0 : ℤ) := by
|
||||
exact h₃f
|
||||
let A := (h₀f.meromorphicAt.order_eq_int_iff 0).1 t₀
|
||||
have : g =ᶠ[𝓝 z₀] (Classical.choose A) := by
|
||||
obtain ⟨h₀, h₁, h₂⟩ := Classical.choose_spec A
|
||||
apply h₁g.localIdentity h₀
|
||||
rw [hn] at h₃g
|
||||
simp at h₃g
|
||||
simp at h₂
|
||||
have h₄g : f =ᶠ[𝓝[≠] z₀] g := by
|
||||
apply Filter.EventuallyEq.filter_mono h₃g
|
||||
exact nhdsWithin_le_nhds
|
||||
exact Filter.EventuallyEq.trans (Filter.EventuallyEq.symm h₄g) h₂
|
||||
exact Filter.EventuallyEq.eq_of_nhds this
|
||||
· simp [h₃f]
|
||||
left
|
||||
apply zero_zpow n
|
||||
by_contra hn
|
||||
rw [hn] at this
|
||||
tauto
|
||||
· exact m₁ (StronglyMeromorphicAt.meromorphicAt hf) z hz
|
||||
|
||||
|
||||
theorem StronglyMeromorphicAt.eliminate
|
||||
{f : ℂ → ℂ}
|
||||
{z₀ : ℂ}
|
||||
(h₁f : StronglyMeromorphicAt f z₀)
|
||||
(h₂f : h₁f.meromorphicAt.order ≠ ⊤) :
|
||||
∃ g : ℂ → ℂ, (AnalyticAt ℂ g z₀)
|
||||
∧ (g z₀ ≠ 0)
|
||||
∧ (f = (fun z ↦ (z-z₀) ^ (h₁f.meromorphicAt.order.untop h₂f)) * g) := by
|
||||
|
||||
let g₁ := (fun z ↦ (z-z₀) ^ (-h₁f.meromorphicAt.order.untop h₂f)) * f
|
||||
let g₁₁ := fun z ↦ (z-z₀) ^ (-h₁f.meromorphicAt.order.untop h₂f)
|
||||
have h₁g₁₁ : MeromorphicAt g₁₁ z₀ := by
|
||||
apply MeromorphicAt.zpow
|
||||
apply AnalyticAt.meromorphicAt
|
||||
apply AnalyticAt.sub
|
||||
apply analyticAt_id
|
||||
exact analyticAt_const
|
||||
have h₂g₁₁ : h₁g₁₁.order = - h₁f.meromorphicAt.order.untop h₂f := by
|
||||
rw [← WithTop.LinearOrderedAddCommGroup.coe_neg]
|
||||
rw [h₁g₁₁.order_eq_int_iff]
|
||||
use 1
|
||||
constructor
|
||||
· exact analyticAt_const
|
||||
· constructor
|
||||
· simp
|
||||
· apply eventually_nhdsWithin_of_forall
|
||||
simp [g₁₁]
|
||||
have h₁g₁ : MeromorphicAt g₁ z₀ := h₁g₁₁.mul h₁f.meromorphicAt
|
||||
have h₂g₁ : h₁g₁.order = 0 := by
|
||||
rw [h₁g₁₁.order_mul h₁f.meromorphicAt]
|
||||
rw [h₂g₁₁]
|
||||
simp
|
||||
rw [add_comm]
|
||||
rw [LinearOrderedAddCommGroupWithTop.add_neg_cancel_of_ne_top h₂f]
|
||||
let g := h₁g₁.makeStronglyMeromorphicAt
|
||||
use g
|
||||
have h₁g : StronglyMeromorphicAt g z₀ := by
|
||||
exact StronglyMeromorphicAt_of_makeStronglyMeromorphic h₁g₁
|
||||
have h₂g : h₁g.meromorphicAt.order = 0 := by
|
||||
rw [← h₁g₁.order_congr (m₂ h₁g₁)]
|
||||
exact h₂g₁
|
||||
constructor
|
||||
· apply analytic
|
||||
· rw [h₂g]
|
||||
· exact h₁g
|
||||
· constructor
|
||||
· rwa [← h₁g.order_eq_zero_iff]
|
||||
· funext z
|
||||
by_cases hz : z = z₀
|
||||
· by_cases hOrd : h₁f.meromorphicAt.order.untop h₂f = 0
|
||||
· simp [hOrd]
|
||||
have : StronglyMeromorphicAt g₁ z₀ := by
|
||||
unfold g₁
|
||||
simp [hOrd]
|
||||
have : (fun z => 1) * f = f := by
|
||||
funext z
|
||||
simp
|
||||
rwa [this]
|
||||
rw [hz]
|
||||
unfold g
|
||||
let A := makeStronglyMeromorphic_id this
|
||||
rw [← A]
|
||||
unfold g₁
|
||||
rw [hOrd]
|
||||
simp
|
||||
· have : h₁f.meromorphicAt.order ≠ 0 := by
|
||||
by_contra hC
|
||||
simp_rw [hC] at hOrd
|
||||
tauto
|
||||
let A := h₁f.order_eq_zero_iff.not.1 this
|
||||
simp at A
|
||||
rw [hz, A]
|
||||
simp
|
||||
left
|
||||
rw [zpow_eq_zero_iff]
|
||||
assumption
|
||||
· simp
|
||||
have : g z = g₁ z := by
|
||||
exact Eq.symm (m₁ h₁g₁ z hz)
|
||||
rw [this]
|
||||
unfold g₁
|
||||
simp [hz]
|
||||
rw [← mul_assoc]
|
||||
rw [mul_inv_cancel₀]
|
||||
simp
|
||||
apply zpow_ne_zero
|
||||
exact sub_ne_zero_of_ne hz
|
||||
|
|
@ -1,173 +0,0 @@
|
|||
import Nevanlinna.meromorphicOn_divisor
|
||||
import Nevanlinna.stronglyMeromorphicAt
|
||||
import Mathlib.Algebra.BigOperators.Finprod
|
||||
|
||||
open Topology
|
||||
|
||||
|
||||
/- Strongly MeromorphicOn -/
|
||||
def StronglyMeromorphicOn
|
||||
(f : ℂ → ℂ)
|
||||
(U : Set ℂ) :=
|
||||
∀ z ∈ U, StronglyMeromorphicAt f z
|
||||
|
||||
|
||||
/- Strongly MeromorphicAt is Meromorphic -/
|
||||
theorem StronglyMeromorphicOn.meromorphicOn
|
||||
{f : ℂ → ℂ}
|
||||
{U : Set ℂ}
|
||||
(hf : StronglyMeromorphicOn f U) :
|
||||
MeromorphicOn f U := by
|
||||
intro z hz
|
||||
exact StronglyMeromorphicAt.meromorphicAt (hf z hz)
|
||||
|
||||
|
||||
/- Strongly MeromorphicOn of non-negative order is analytic -/
|
||||
theorem StronglyMeromorphicOn.analytic
|
||||
{f : ℂ → ℂ}
|
||||
{U : Set ℂ}
|
||||
(h₁f : StronglyMeromorphicOn f U)
|
||||
(h₂f : ∀ x, (hx : x ∈ U) → 0 ≤ (h₁f x hx).meromorphicAt.order):
|
||||
∀ z ∈ U, AnalyticAt ℂ f z := by
|
||||
intro z hz
|
||||
apply StronglyMeromorphicAt.analytic
|
||||
exact h₂f z hz
|
||||
exact h₁f z hz
|
||||
|
||||
|
||||
/- Analytic functions are strongly meromorphic -/
|
||||
theorem AnalyticOn.stronglyMeromorphicOn
|
||||
{f : ℂ → ℂ}
|
||||
{U : Set ℂ}
|
||||
(h₁f : AnalyticOnNhd ℂ f U) :
|
||||
StronglyMeromorphicOn f U := by
|
||||
intro z hz
|
||||
apply AnalyticAt.stronglyMeromorphicAt
|
||||
exact h₁f z hz
|
||||
|
||||
|
||||
/- Make strongly MeromorphicAt -/
|
||||
noncomputable def MeromorphicOn.makeStronglyMeromorphicOn
|
||||
{f : ℂ → ℂ}
|
||||
{U : Set ℂ}
|
||||
(hf : MeromorphicOn f U) :
|
||||
ℂ → ℂ := by
|
||||
intro z
|
||||
by_cases hz : z ∈ U
|
||||
· exact (hf z hz).makeStronglyMeromorphicAt z
|
||||
· exact f z
|
||||
|
||||
|
||||
theorem makeStronglyMeromorphicOn_changeDiscrete
|
||||
{f : ℂ → ℂ}
|
||||
{U : Set ℂ}
|
||||
{z₀ : ℂ}
|
||||
(hf : MeromorphicOn f U)
|
||||
(hz₀ : z₀ ∈ U) :
|
||||
hf.makeStronglyMeromorphicOn =ᶠ[𝓝[≠] z₀] f := by
|
||||
apply Filter.eventually_iff_exists_mem.2
|
||||
let A := (hf z₀ hz₀).eventually_analyticAt
|
||||
obtain ⟨V, h₁V, h₂V⟩ := Filter.eventually_iff_exists_mem.1 A
|
||||
use V
|
||||
constructor
|
||||
· assumption
|
||||
· intro v hv
|
||||
unfold MeromorphicOn.makeStronglyMeromorphicOn
|
||||
by_cases h₂v : v ∈ U
|
||||
· simp [h₂v]
|
||||
rw [← StronglyMeromorphicAt.makeStronglyMeromorphic_id]
|
||||
exact AnalyticAt.stronglyMeromorphicAt (h₂V v hv)
|
||||
· simp [h₂v]
|
||||
|
||||
|
||||
theorem analyticAt_ratlPolynomial₁
|
||||
{z : ℂ}
|
||||
(d : ℂ → ℤ)
|
||||
(P : Finset ℂ) :
|
||||
z ∉ P → AnalyticAt ℂ (∏ u ∈ P, fun z ↦ (z - u) ^ d u) z := by
|
||||
intro hz
|
||||
rw [Finset.prod_fn]
|
||||
apply Finset.analyticAt_prod
|
||||
intro u hu
|
||||
apply AnalyticAt.zpow
|
||||
apply AnalyticAt.sub
|
||||
apply analyticAt_id
|
||||
apply analyticAt_const
|
||||
rw [sub_ne_zero, ne_comm]
|
||||
exact ne_of_mem_of_not_mem hu hz
|
||||
|
||||
|
||||
theorem stronglyMeromorphicOn_ratlPolynomial₂
|
||||
{U : Set ℂ}
|
||||
(d : ℂ → ℤ)
|
||||
(P : Finset ℂ) :
|
||||
StronglyMeromorphicOn (∏ u ∈ P, fun z ↦ (z - u) ^ d u) U := by
|
||||
|
||||
intro z hz
|
||||
by_cases h₂z : z ∈ P
|
||||
· rw [← Finset.mul_prod_erase P _ h₂z]
|
||||
right
|
||||
use d z
|
||||
use ∏ x ∈ P.erase z, fun z => (z - x) ^ d x
|
||||
constructor
|
||||
· have : z ∉ P.erase z := Finset.not_mem_erase z P
|
||||
apply analyticAt_ratlPolynomial₁ d (P.erase z) this
|
||||
· constructor
|
||||
· simp only [Finset.prod_apply]
|
||||
rw [Finset.prod_ne_zero_iff]
|
||||
intro u hu
|
||||
apply zpow_ne_zero
|
||||
rw [sub_ne_zero]
|
||||
by_contra hCon
|
||||
rw [hCon] at hu
|
||||
let A := Finset.not_mem_erase u P
|
||||
tauto
|
||||
· exact Filter.Eventually.of_forall (congrFun rfl)
|
||||
· apply AnalyticAt.stronglyMeromorphicAt
|
||||
exact analyticAt_ratlPolynomial₁ d P (z := z) h₂z
|
||||
|
||||
|
||||
|
||||
theorem stronglyMeromorphicOn_ratlPolynomial₃
|
||||
{U : Set ℂ}
|
||||
(d : ℂ → ℤ) :
|
||||
StronglyMeromorphicOn (∏ᶠ u, fun z ↦ (z - u) ^ d u) U := by
|
||||
by_cases hd : (Function.mulSupport fun u z => (z - u) ^ d u).Finite
|
||||
· rw [finprod_eq_prod _ hd]
|
||||
apply stronglyMeromorphicOn_ratlPolynomial₂ (U := U) d hd.toFinset
|
||||
· rw [finprod_of_infinite_mulSupport hd]
|
||||
apply AnalyticOn.stronglyMeromorphicOn
|
||||
apply analyticOnNhd_const
|
||||
|
||||
|
||||
theorem stronglyMeromorphicOn_divisor_ratlPolynomial
|
||||
{U : Set ℂ}
|
||||
(d : ℂ → ℤ)
|
||||
(hd : Set.Finite d.support) :
|
||||
(stronglyMeromorphicOn_ratlPolynomial₃ d (U := U)).meromorphicOn.divisor = d := by
|
||||
sorry
|
||||
|
||||
|
||||
theorem makeStronglyMeromorphicOn_changeDiscrete'
|
||||
{f : ℂ → ℂ}
|
||||
{U : Set ℂ}
|
||||
{z₀ : ℂ}
|
||||
(hf : MeromorphicOn f U)
|
||||
(hz₀ : z₀ ∈ U) :
|
||||
hf.makeStronglyMeromorphicOn =ᶠ[𝓝 z₀] (hf z₀ hz₀).makeStronglyMeromorphicAt := by
|
||||
apply Mnhds
|
||||
let A := makeStronglyMeromorphicOn_changeDiscrete hf hz₀
|
||||
apply Filter.EventuallyEq.trans A
|
||||
exact m₂ (hf z₀ hz₀)
|
||||
unfold MeromorphicOn.makeStronglyMeromorphicOn
|
||||
simp [hz₀]
|
||||
|
||||
|
||||
theorem StronglyMeromorphicOn_of_makeStronglyMeromorphicOn
|
||||
{f : ℂ → ℂ}
|
||||
{U : Set ℂ}
|
||||
(hf : MeromorphicOn f U) :
|
||||
StronglyMeromorphicOn hf.makeStronglyMeromorphicOn U := by
|
||||
intro z₀ hz₀
|
||||
rw [stronglyMeromorphicAt_congr (makeStronglyMeromorphicOn_changeDiscrete' hf hz₀)]
|
||||
exact StronglyMeromorphicAt_of_makeStronglyMeromorphic (hf z₀ hz₀)
|
||||
|
|
@ -1,345 +0,0 @@
|
|||
import Mathlib.Analysis.Analytic.Meromorphic
|
||||
import Mathlib.Data.Set.Finite
|
||||
import Nevanlinna.analyticAt
|
||||
import Nevanlinna.divisor
|
||||
import Nevanlinna.meromorphicAt
|
||||
import Nevanlinna.meromorphicOn
|
||||
import Nevanlinna.meromorphicOn_divisor
|
||||
import Nevanlinna.stronglyMeromorphicOn
|
||||
import Nevanlinna.mathlibAddOn
|
||||
|
||||
open scoped Interval Topology
|
||||
open Real Filter MeasureTheory intervalIntegral
|
||||
|
||||
theorem MeromorphicOn.decompose₁
|
||||
{f : ℂ → ℂ}
|
||||
{U : Set ℂ}
|
||||
{z₀ : ℂ}
|
||||
(h₁f : MeromorphicOn f U)
|
||||
(h₂f : StronglyMeromorphicAt f z₀)
|
||||
(h₃f : h₂f.meromorphicAt.order ≠ ⊤)
|
||||
(hz₀ : z₀ ∈ U) :
|
||||
∃ g : ℂ → ℂ, (MeromorphicOn g U)
|
||||
∧ (AnalyticAt ℂ g z₀)
|
||||
∧ (g z₀ ≠ 0)
|
||||
∧ (f = g * fun z ↦ (z - z₀) ^ (h₁f.divisor z₀)) := by
|
||||
|
||||
let h₁ := fun z ↦ (z - z₀) ^ (-h₁f.divisor z₀)
|
||||
have h₁h₁ : MeromorphicOn h₁ U := by
|
||||
apply MeromorphicOn.zpow
|
||||
apply AnalyticOnNhd.meromorphicOn
|
||||
apply AnalyticOnNhd.sub
|
||||
exact analyticOnNhd_id
|
||||
exact analyticOnNhd_const
|
||||
let n : ℤ := (-h₁f.divisor z₀)
|
||||
have h₂h₁ : (h₁h₁ z₀ hz₀).order = n := by
|
||||
simp_rw [(h₁h₁ z₀ hz₀).order_eq_int_iff]
|
||||
use 1
|
||||
constructor
|
||||
· apply analyticAt_const
|
||||
· constructor
|
||||
· simp
|
||||
· apply eventually_nhdsWithin_of_forall
|
||||
intro z hz
|
||||
simp
|
||||
|
||||
let g₁ := f * h₁
|
||||
have h₁g₁ : MeromorphicOn g₁ U := by
|
||||
apply h₁f.mul h₁h₁
|
||||
have h₂g₁ : (h₁g₁ z₀ hz₀).order = 0 := by
|
||||
rw [(h₁f z₀ hz₀).order_mul (h₁h₁ z₀ hz₀)]
|
||||
rw [h₂h₁]
|
||||
unfold n
|
||||
rw [MeromorphicOn.divisor_def₂ h₁f hz₀ h₃f]
|
||||
conv =>
|
||||
left
|
||||
left
|
||||
rw [Eq.symm (WithTop.coe_untop (h₁f z₀ hz₀).order h₃f)]
|
||||
have
|
||||
(a b c : ℤ)
|
||||
(h : a + b = c) :
|
||||
(a : WithTop ℤ) + (b : WithTop ℤ) = (c : WithTop ℤ) := by
|
||||
rw [← h]
|
||||
simp
|
||||
rw [this ((h₁f z₀ hz₀).order.untop h₃f) (-(h₁f z₀ hz₀).order.untop h₃f) 0]
|
||||
simp
|
||||
ring
|
||||
|
||||
let g := (h₁g₁ z₀ hz₀).makeStronglyMeromorphicAt
|
||||
have h₂g : StronglyMeromorphicAt g z₀ := by
|
||||
exact StronglyMeromorphicAt_of_makeStronglyMeromorphic (h₁g₁ z₀ hz₀)
|
||||
have h₁g : MeromorphicOn g U := by
|
||||
intro z hz
|
||||
by_cases h₁z : z = z₀
|
||||
· rw [h₁z]
|
||||
apply h₂g.meromorphicAt
|
||||
· apply (h₁g₁ z hz).congr
|
||||
rw [eventuallyEq_nhdsWithin_iff]
|
||||
rw [eventually_nhds_iff]
|
||||
use {z₀}ᶜ
|
||||
constructor
|
||||
· intro y h₁y h₂y
|
||||
let A := m₁ (h₁g₁ z₀ hz₀) y h₁y
|
||||
unfold g
|
||||
rw [← A]
|
||||
· constructor
|
||||
· exact isOpen_compl_singleton
|
||||
· exact h₁z
|
||||
have h₃g : (h₁g z₀ hz₀).order = 0 := by
|
||||
unfold g
|
||||
let B := m₂ (h₁g₁ z₀ hz₀)
|
||||
let A := (h₁g₁ z₀ hz₀).order_congr B
|
||||
rw [← A]
|
||||
rw [h₂g₁]
|
||||
have h₄g : AnalyticAt ℂ g z₀ := by
|
||||
apply h₂g.analytic
|
||||
rw [h₃g]
|
||||
|
||||
use g
|
||||
constructor
|
||||
· exact h₁g
|
||||
· constructor
|
||||
· exact h₄g
|
||||
· constructor
|
||||
· exact (h₂g.order_eq_zero_iff).mp h₃g
|
||||
· funext z
|
||||
by_cases hz : z = z₀
|
||||
· rw [hz]
|
||||
simp
|
||||
by_cases h : h₁f.divisor z₀ = 0
|
||||
· simp [h]
|
||||
have h₂h₁ : h₁ = 1 := by
|
||||
funext w
|
||||
unfold h₁
|
||||
simp [h]
|
||||
have h₃g₁ : g₁ = f := by
|
||||
unfold g₁
|
||||
rw [h₂h₁]
|
||||
simp
|
||||
have h₄g₁ : StronglyMeromorphicAt g₁ z₀ := by
|
||||
rwa [h₃g₁]
|
||||
let A := h₄g₁.makeStronglyMeromorphic_id
|
||||
unfold g
|
||||
rw [← A, h₃g₁]
|
||||
· have : (0 : ℂ) ^ h₁f.divisor z₀ = (0 : ℂ) := by
|
||||
exact zero_zpow (h₁f.divisor z₀) h
|
||||
rw [this]
|
||||
simp
|
||||
let A := h₂f.order_eq_zero_iff.not
|
||||
simp at A
|
||||
rw [← A]
|
||||
unfold MeromorphicOn.divisor at h
|
||||
simp [hz₀] at h
|
||||
exact h.1
|
||||
· simp
|
||||
let B := m₁ (h₁g₁ z₀ hz₀) z hz
|
||||
unfold g
|
||||
rw [← B]
|
||||
unfold g₁ h₁
|
||||
simp [hz]
|
||||
rw [mul_assoc]
|
||||
rw [inv_mul_cancel₀]
|
||||
simp
|
||||
apply zpow_ne_zero
|
||||
rwa [sub_ne_zero]
|
||||
|
||||
|
||||
theorem MeromorphicOn.decompose₂
|
||||
{f : ℂ → ℂ}
|
||||
{U : Set ℂ}
|
||||
{P : Finset U}
|
||||
(hf : StronglyMeromorphicOn f U) :
|
||||
(∀ p ∈ P, (hf p p.2).meromorphicAt.order ≠ ⊤) →
|
||||
∃ g : ℂ → ℂ, (MeromorphicOn g U)
|
||||
∧ (∀ p : P, AnalyticAt ℂ g p)
|
||||
∧ (∀ p : P, g p ≠ 0)
|
||||
∧ (f = g * ∏ p : P, fun z ↦ (z - p.1.1) ^ (hf.meromorphicOn.divisor p.1.1)) := by
|
||||
|
||||
apply Finset.induction (p := fun (P : Finset U) ↦
|
||||
(∀ p ∈ P, (hf p p.2).meromorphicAt.order ≠ ⊤) →
|
||||
∃ g : ℂ → ℂ, (MeromorphicOn g U)
|
||||
∧ (∀ p : P, AnalyticAt ℂ g p)
|
||||
∧ (∀ p : P, g p ≠ 0)
|
||||
∧ (f = g * ∏ p : P, fun z ↦ (z - p.1.1) ^ (hf.meromorphicOn.divisor p.1.1)))
|
||||
|
||||
-- case empty
|
||||
simp
|
||||
exact hf.meromorphicOn
|
||||
|
||||
-- case insert
|
||||
intro u P hu iHyp
|
||||
intro hOrder
|
||||
obtain ⟨g₀, h₁g₀, h₂g₀, h₃g₀, h₄g₀⟩ := iHyp (fun p hp ↦ hOrder p (Finset.mem_insert_of_mem hp))
|
||||
|
||||
have h₀ : AnalyticAt ℂ (∏ p : P, fun z ↦ (z - p.1.1) ^ (hf.meromorphicOn.divisor p.1.1)) u := by
|
||||
have : (∏ p : P, fun z ↦ (z - p.1.1) ^ (hf.meromorphicOn.divisor p.1.1)) = (fun z => ∏ p : P, (z - p.1.1) ^ (hf.meromorphicOn.divisor p.1.1)) := by
|
||||
funext w
|
||||
simp
|
||||
rw [this]
|
||||
apply Finset.analyticAt_prod
|
||||
intro p hp
|
||||
apply AnalyticAt.zpow
|
||||
apply AnalyticAt.sub
|
||||
apply analyticAt_id
|
||||
apply analyticAt_const
|
||||
by_contra hCon
|
||||
rw [sub_eq_zero] at hCon
|
||||
have : p.1 = u := by
|
||||
exact SetCoe.ext (_root_.id (Eq.symm hCon))
|
||||
rw [← this] at hu
|
||||
simp [hp] at hu
|
||||
|
||||
have h₁ : (∏ p : P, fun z ↦ (z - p.1.1) ^ (hf.meromorphicOn.divisor p.1.1)) u ≠ 0 := by
|
||||
simp only [Finset.prod_apply]
|
||||
rw [Finset.prod_ne_zero_iff]
|
||||
intro p hp
|
||||
apply zpow_ne_zero
|
||||
by_contra hCon
|
||||
rw [sub_eq_zero] at hCon
|
||||
have : p.1 = u := by
|
||||
exact SetCoe.ext (_root_.id (Eq.symm hCon))
|
||||
rw [← this] at hu
|
||||
simp [hp] at hu
|
||||
|
||||
have h₅g₀ : StronglyMeromorphicAt g₀ u := by
|
||||
rw [stronglyMeromorphicAt_of_mul_analytic h₀ h₁]
|
||||
rw [← h₄g₀]
|
||||
exact hf u u.2
|
||||
|
||||
have h₆g₀ : (h₁g₀ u u.2).order ≠ ⊤ := by
|
||||
by_contra hCon
|
||||
let A := (h₁g₀ u u.2).order_mul h₀.meromorphicAt
|
||||
simp_rw [← h₄g₀, hCon] at A
|
||||
simp at A
|
||||
let B := hOrder u (Finset.mem_insert_self u P)
|
||||
tauto
|
||||
|
||||
obtain ⟨g, h₁g, h₂g, h₃g, h₄g⟩ := h₁g₀.decompose₁ h₅g₀ h₆g₀ u.2
|
||||
use g
|
||||
· constructor
|
||||
· exact h₁g
|
||||
· constructor
|
||||
· intro ⟨v₁, v₂⟩
|
||||
simp
|
||||
simp at v₂
|
||||
rcases v₂ with hv|hv
|
||||
· rwa [hv]
|
||||
· let A := h₂g₀ ⟨v₁, hv⟩
|
||||
rw [h₄g] at A
|
||||
rw [← analyticAt_of_mul_analytic] at A
|
||||
simp at A
|
||||
exact A
|
||||
--
|
||||
simp
|
||||
apply AnalyticAt.zpow
|
||||
apply AnalyticAt.sub
|
||||
apply analyticAt_id
|
||||
apply analyticAt_const
|
||||
by_contra hCon
|
||||
rw [sub_eq_zero] at hCon
|
||||
|
||||
have : v₁ = u := by
|
||||
exact SetCoe.ext hCon
|
||||
rw [this] at hv
|
||||
tauto
|
||||
--
|
||||
apply zpow_ne_zero
|
||||
simp
|
||||
by_contra hCon
|
||||
rw [sub_eq_zero] at hCon
|
||||
have : v₁ = u := by
|
||||
exact SetCoe.ext hCon
|
||||
rw [this] at hv
|
||||
tauto
|
||||
|
||||
· constructor
|
||||
· intro ⟨v₁, v₂⟩
|
||||
simp
|
||||
simp at v₂
|
||||
rcases v₂ with hv|hv
|
||||
· rwa [hv]
|
||||
· by_contra hCon
|
||||
let A := h₃g₀ ⟨v₁,hv⟩
|
||||
rw [h₄g] at A
|
||||
simp at A
|
||||
tauto
|
||||
· conv =>
|
||||
left
|
||||
rw [h₄g₀, h₄g]
|
||||
simp
|
||||
rw [mul_assoc]
|
||||
congr
|
||||
rw [Finset.prod_insert]
|
||||
simp
|
||||
congr
|
||||
have : (hf u u.2).meromorphicAt.order = (h₁g₀ u u.2).order := by
|
||||
have h₅g₀ : f =ᶠ[𝓝 u.1] (g₀ * ∏ p : P, fun z => (z - p.1.1) ^ (hf.meromorphicOn.divisor p.1.1)) := by
|
||||
exact Eq.eventuallyEq h₄g₀
|
||||
have h₆g₀ : f =ᶠ[𝓝[≠] u.1] (g₀ * ∏ p : P, fun z => (z - p.1.1) ^ (hf.meromorphicOn.divisor p.1.1)) := by
|
||||
exact eventuallyEq_nhdsWithin_of_eqOn fun ⦃x⦄ a => congrFun h₄g₀ x
|
||||
rw [(hf u u.2).meromorphicAt.order_congr h₆g₀]
|
||||
let C := (h₁g₀ u u.2).order_mul h₀.meromorphicAt
|
||||
rw [C]
|
||||
let D := h₀.order_eq_zero_iff.2 h₁
|
||||
let E := h₀.meromorphicAt_order
|
||||
rw [E, D]
|
||||
simp
|
||||
have : hf.meromorphicOn.divisor u = h₁g₀.divisor u := by
|
||||
unfold MeromorphicOn.divisor
|
||||
simp
|
||||
rw [this]
|
||||
rw [this]
|
||||
--
|
||||
simpa
|
||||
|
||||
|
||||
theorem MeromorphicOn.decompose₃
|
||||
{f : ℂ → ℂ}
|
||||
{U : Set ℂ}
|
||||
(h₁U : IsCompact U)
|
||||
(h₂U : IsConnected U)
|
||||
(h₁f : StronglyMeromorphicOn f U)
|
||||
(h₂f : ∃ u : U, f u ≠ 0) :
|
||||
∃ g : ℂ → ℂ, (MeromorphicOn g U)
|
||||
∧ (AnalyticOn ℂ g U)
|
||||
∧ (∀ u : U, g u ≠ 0)
|
||||
∧ (f = g * ∏ᶠ u, fun z ↦ (z - u) ^ (h₁f.meromorphicOn.divisor u)) := by
|
||||
|
||||
have h₃f : ∀ u : U, (h₁f u u.2).meromorphicAt.order ≠ ⊤ := by
|
||||
apply MeromorphicOn.order_ne_top h₂U h₁f h₂f
|
||||
|
||||
have h₄f : Set.Finite (Function.support h₁f.meromorphicOn.divisor) := by
|
||||
exact h₁f.meromorphicOn.divisor.finiteSupport h₁U
|
||||
|
||||
let P' : Set U := Subtype.val ⁻¹' Function.support h₁f.meromorphicOn.divisor
|
||||
let P := (h₄f.preimage Set.injOn_subtype_val : Set.Finite P').toFinset
|
||||
have hP : ∀ p ∈ P, (h₁f p p.2).meromorphicAt.order ≠ ⊤ := by
|
||||
intro p hp
|
||||
apply h₃f
|
||||
|
||||
obtain ⟨g, h₁g, h₂g, h₃g, h₄g⟩ := MeromorphicOn.decompose₂ h₁f (P := P) hP
|
||||
|
||||
let h := ∏ p ∈ P, fun z => (z - p.1) ^ h₁f.meromorphicOn.divisor p.1
|
||||
|
||||
have h₂h : StronglyMeromorphicOn h U := by
|
||||
unfold h
|
||||
apply stronglyMeromorphicOn_ratlPolynomial₂
|
||||
have h₁h : MeromorphicOn h U := by
|
||||
exact StronglyMeromorphicOn.meromorphicOn h₂h
|
||||
have h₃h : h₁h.divisor = h₁f.meromorphicOn.divisor := by
|
||||
sorry
|
||||
|
||||
|
||||
use g
|
||||
constructor
|
||||
· exact h₁g
|
||||
· constructor
|
||||
· sorry
|
||||
· constructor
|
||||
· sorry
|
||||
· conv =>
|
||||
left
|
||||
rw [h₄g]
|
||||
congr
|
||||
simp
|
||||
sorry
|
||||
|
|
@ -5,17 +5,17 @@
|
|||
"type": "git",
|
||||
"subDir": null,
|
||||
"scope": "leanprover-community",
|
||||
"rev": "b100ff2565805e9f30a482788b3fc66937a7f38a",
|
||||
"rev": "46fed98b5cac2b1ea64e363b420c382ed1af0d85",
|
||||
"name": "batteries",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inputRev": "main",
|
||||
"inherited": true,
|
||||
"configFile": "lakefile.toml"},
|
||||
"configFile": "lakefile.lean"},
|
||||
{"url": "https://github.com/leanprover-community/quote4",
|
||||
"type": "git",
|
||||
"subDir": null,
|
||||
"scope": "leanprover-community",
|
||||
"rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41",
|
||||
"rev": "2c8ae451ce9ffc83554322b14437159c1a9703f9",
|
||||
"name": "Qq",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inputRev": "master",
|
||||
|
|
@ -25,7 +25,7 @@
|
|||
"type": "git",
|
||||
"subDir": null,
|
||||
"scope": "leanprover-community",
|
||||
"rev": "de91b59101763419997026c35a41432ac8691f15",
|
||||
"rev": "662f986ad3c5ad6ab1a1726b3c04f5ec425aa9f7",
|
||||
"name": "aesop",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inputRev": "master",
|
||||
|
|
@ -35,17 +35,17 @@
|
|||
"type": "git",
|
||||
"subDir": null,
|
||||
"scope": "leanprover-community",
|
||||
"rev": "1383e72b40dd62a566896a6e348ffe868801b172",
|
||||
"rev": "eb08eee94098fe530ccd6d8751a86fe405473d4c",
|
||||
"name": "proofwidgets",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inputRev": "v0.0.46",
|
||||
"inputRev": "v0.0.42",
|
||||
"inherited": true,
|
||||
"configFile": "lakefile.lean"},
|
||||
{"url": "https://github.com/leanprover/lean4-cli",
|
||||
"type": "git",
|
||||
"subDir": null,
|
||||
"scope": "leanprover",
|
||||
"rev": "726b3c9ad13acca724d4651f14afc4804a7b0e4d",
|
||||
"scope": "",
|
||||
"rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
|
||||
"name": "Cli",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inputRev": "main",
|
||||
|
|
@ -55,37 +55,27 @@
|
|||
"type": "git",
|
||||
"subDir": null,
|
||||
"scope": "leanprover-community",
|
||||
"rev": "b0b73e5bc33f1bc4d3c0f254630dd0e262cecc08",
|
||||
"rev": "fb7841a6f4fb389ec0e47dd4677844d49906af3c",
|
||||
"name": "importGraph",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inputRev": "main",
|
||||
"inherited": true,
|
||||
"configFile": "lakefile.toml"},
|
||||
{"url": "https://github.com/leanprover-community/LeanSearchClient",
|
||||
{"url": "https://github.com/siddhartha-gadgil/LeanSearchClient.git",
|
||||
"type": "git",
|
||||
"subDir": null,
|
||||
"scope": "leanprover-community",
|
||||
"rev": "86d0d0584f5cd165353e2f8a30c455cd0e168ac2",
|
||||
"scope": "",
|
||||
"rev": "c260ed920e2ebd23ef9fc8ca3fd24115e04c18b1",
|
||||
"name": "LeanSearchClient",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inputRev": "main",
|
||||
"inherited": true,
|
||||
"configFile": "lakefile.toml"},
|
||||
{"url": "https://github.com/leanprover-community/plausible",
|
||||
"type": "git",
|
||||
"subDir": null,
|
||||
"scope": "leanprover-community",
|
||||
"rev": "42dc02bdbc5d0c2f395718462a76c3d87318f7fa",
|
||||
"name": "plausible",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inputRev": "main",
|
||||
"inherited": true,
|
||||
"configFile": "lakefile.toml"},
|
||||
{"url": "https://github.com/leanprover-community/mathlib4.git",
|
||||
"type": "git",
|
||||
"subDir": null,
|
||||
"scope": "",
|
||||
"rev": "e3d7d7f053ea862ffb7d1613eff6de0f2e3e8e14",
|
||||
"rev": "4e40837aec257729b3c38dc3e635fc64a7a8a8c1",
|
||||
"name": "mathlib",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inputRev": null,
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
leanprover/lean4:v4.14.0-rc2
|
||||
leanprover/lean4:v4.12.0-rc1
|
||||
|
|
|
|||
Loading…
Reference in New Issue