From e3853f1632450402f8bcbd6f0d9ae10512ed7516 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Mon, 9 Sep 2024 12:45:07 +0200 Subject: [PATCH] Update Mathlib --- Nevanlinna/analyticOn_zeroSet2.lean | 449 ++++++++++++++++++ Nevanlinna/laplace.lean | 8 +- Nevanlinna/periodic_integrability.lean | 4 +- .../specialFunctions_Integral_log_sin.lean | 1 + 4 files changed, 456 insertions(+), 6 deletions(-) create mode 100644 Nevanlinna/analyticOn_zeroSet2.lean diff --git a/Nevanlinna/analyticOn_zeroSet2.lean b/Nevanlinna/analyticOn_zeroSet2.lean new file mode 100644 index 0000000..94c65bf --- /dev/null +++ b/Nevanlinna/analyticOn_zeroSet2.lean @@ -0,0 +1,449 @@ +import Mathlib.Analysis.Analytic.Constructions +import Mathlib.Analysis.Analytic.IsolatedZeros +import Mathlib.Analysis.Complex.Basic + + +theorem AnalyticOn.order_eq_nat_iff + {f : ℂ → ℂ} + {U : Set ℂ} + {z₀ : ℂ} + (hf : AnalyticOn ℂ f U) + (hz₀ : z₀ ∈ U) + (n : ℕ) : + (hf z₀ hz₀).order = ↑n ↔ ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ g z₀ ≠ 0 ∧ ∀ z, f z = (z - z₀) ^ n • g z := by + + constructor + -- Direction → + intro hn + obtain ⟨gloc, h₁gloc, h₂gloc, h₃gloc⟩ := (AnalyticAt.order_eq_nat_iff (hf z₀ hz₀) n).1 hn + + -- Define a candidate function; this is (f z) / (z - z₀) ^ n with the + -- removable singularity removed + let g : ℂ → ℂ := fun z ↦ if z = z₀ then gloc z₀ else (f z) / (z - z₀) ^ n + + -- Describe g near z₀ + have g_near_z₀ : ∀ᶠ (z : ℂ) in nhds z₀, g z = gloc z := by + rw [eventually_nhds_iff] + obtain ⟨t, h₁t, h₂t, h₃t⟩ := eventually_nhds_iff.1 h₃gloc + use t + constructor + · intro y h₁y + by_cases h₂y : y = z₀ + · dsimp [g]; simp [h₂y] + · dsimp [g]; simp [h₂y] + rw [div_eq_iff_mul_eq, eq_comm, mul_comm] + exact h₁t y h₁y + norm_num + rw [sub_eq_zero] + tauto + · constructor + · assumption + · assumption + + -- Describe g near points z₁ that are different from z₀ + have g_near_z₁ {z₁ : ℂ} : z₁ ≠ z₀ → ∀ᶠ (z : ℂ) in nhds z₁, g z = f z / (z - z₀) ^ n := by + intro hz₁ + rw [eventually_nhds_iff] + use {z₀}ᶜ + constructor + · intro y hy + simp at hy + simp [g, hy] + · exact ⟨isOpen_compl_singleton, hz₁⟩ + + -- Use g and show that it has all required properties + use g + constructor + · -- AnalyticOn ℂ g U + intro z h₁z + by_cases h₂z : z = z₀ + · rw [h₂z] + apply AnalyticAt.congr h₁gloc + exact Filter.EventuallyEq.symm g_near_z₀ + · simp_rw [eq_comm] at g_near_z₁ + apply AnalyticAt.congr _ (g_near_z₁ h₂z) + apply AnalyticAt.div + exact hf z h₁z + apply AnalyticAt.pow + apply AnalyticAt.sub + apply analyticAt_id + apply analyticAt_const + simp + rw [sub_eq_zero] + tauto + · constructor + · simp [g]; tauto + · intro z + by_cases h₂z : z = z₀ + · rw [h₂z, g_near_z₀.self_of_nhds] + exact h₃gloc.self_of_nhds + · rw [(g_near_z₁ h₂z).self_of_nhds] + simp [h₂z] + rw [div_eq_mul_inv, mul_comm, mul_assoc, inv_mul_cancel₀] + simp; norm_num + rw [sub_eq_zero] + tauto + + -- direction ← + intro h + obtain ⟨g, h₁g, h₂g, h₃g⟩ := h + rw [AnalyticAt.order_eq_nat_iff] + use g + exact ⟨h₁g z₀ hz₀, ⟨h₂g, Filter.Eventually.of_forall h₃g⟩⟩ + + +theorem AnalyticAt.order_mul + {f₁ f₂ : ℂ → ℂ} + {z₀ : ℂ} + (hf₁ : AnalyticAt ℂ f₁ z₀) + (hf₂ : AnalyticAt ℂ f₂ z₀) : + (AnalyticAt.mul hf₁ hf₂).order = hf₁.order + hf₂.order := by + by_cases h₂f₁ : hf₁.order = ⊤ + · simp [h₂f₁] + rw [AnalyticAt.order_eq_top_iff, eventually_nhds_iff] + rw [AnalyticAt.order_eq_top_iff, eventually_nhds_iff] at h₂f₁ + obtain ⟨t, h₁t, h₂t, h₃t⟩ := h₂f₁ + use t + constructor + · intro y hy + rw [h₁t y hy] + ring + · exact ⟨h₂t, h₃t⟩ + · by_cases h₂f₂ : hf₂.order = ⊤ + · simp [h₂f₂] + rw [AnalyticAt.order_eq_top_iff, eventually_nhds_iff] + rw [AnalyticAt.order_eq_top_iff, eventually_nhds_iff] at h₂f₂ + obtain ⟨t, h₁t, h₂t, h₃t⟩ := h₂f₂ + use t + constructor + · intro y hy + rw [h₁t y hy] + ring + · exact ⟨h₂t, h₃t⟩ + · obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (AnalyticAt.order_eq_nat_iff hf₁ ↑hf₁.order.toNat).1 (eq_comm.1 (ENat.coe_toNat h₂f₁)) + obtain ⟨g₂, h₁g₂, h₂g₂, h₃g₂⟩ := (AnalyticAt.order_eq_nat_iff hf₂ ↑hf₂.order.toNat).1 (eq_comm.1 (ENat.coe_toNat h₂f₂)) + rw [← ENat.coe_toNat h₂f₁, ← ENat.coe_toNat h₂f₂, ← ENat.coe_add] + rw [AnalyticAt.order_eq_nat_iff (AnalyticAt.mul hf₁ hf₂) ↑(hf₁.order.toNat + hf₂.order.toNat)] + 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 h₃g₁ + obtain ⟨t₂, h₁t₂, h₂t₂, h₃t₂⟩ := eventually_nhds_iff.1 h₃g₂ + rw [eventually_nhds_iff] + use t₁ ∩ t₂ + constructor + · intro y hy + rw [h₁t₁ y hy.1, h₁t₂ y hy.2] + simp; ring + · constructor + · exact IsOpen.inter h₂t₁ h₂t₂ + · exact Set.mem_inter h₃t₁ h₃t₂ + + +theorem AnalyticOn.eliminateZeros + {f : ℂ → ℂ} + {U : Set ℂ} + {A : Finset U} + (hf : AnalyticOn ℂ f U) + (n : ℂ → ℕ) : + (∀ 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 := by + + 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 + use f + simp + exact hf + + -- case insert + intro b₀ B hb iHyp + intro hBinsert + obtain ⟨g₀, h₁g₀, h₂g₀, h₃g₀⟩ := iHyp (fun a ha ↦ hBinsert a (Finset.mem_insert_of_mem ha)) + + have : (h₁g₀ b₀ b₀.2).order = n b₀ := by + + rw [← hBinsert b₀ (Finset.mem_insert_self b₀ B)] + + let φ := fun z ↦ (∏ a ∈ B, (z - a.1) ^ n a.1) + + have : f = fun z ↦ φ z * g₀ z := by + funext z + rw [h₃g₀ z] + rfl + simp_rw [this] + + have h₁φ : AnalyticAt ℂ φ b₀ := by + dsimp [φ] + apply Finset.analyticAt_prod + intro b _ + apply AnalyticAt.pow + apply AnalyticAt.sub + apply analyticAt_id ℂ + exact analyticAt_const + + have h₂φ : h₁φ.order = (0 : ℕ) := by + rw [AnalyticAt.order_eq_nat_iff h₁φ 0] + use φ + constructor + · assumption + · constructor + · dsimp [φ] + push_neg + rw [Finset.prod_ne_zero_iff] + intro a ha + simp + have : ¬ (b₀.1 - a.1 = 0) := by + by_contra C + rw [sub_eq_zero] at C + rw [SetCoe.ext C] at hb + tauto + tauto + · simp + + rw [AnalyticAt.order_mul h₁φ (h₁g₀ b₀ b₀.2)] + + rw [h₂φ] + simp + + + obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (AnalyticOn.order_eq_nat_iff h₁g₀ b₀.2 (n b₀)).1 this + + use g₁ + constructor + · exact h₁g₁ + · constructor + · intro a h₁a + by_cases h₂a : a = b₀ + · rwa [h₂a] + · let A' := Finset.mem_of_mem_insert_of_ne h₁a h₂a + let B' := h₃g₁ a + let C' := h₂g₀ a A' + rw [B'] at C' + exact right_ne_zero_of_smul C' + · intro z + let A' := h₃g₀ z + rw [h₃g₁ z] at A' + rw [A'] + rw [← smul_assoc] + congr + simp + rw [Finset.prod_insert] + ring + exact hb + + +theorem XX + {f : ℂ → ℂ} + {U : Set ℂ} + (hU : IsPreconnected 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 + + intro hu + apply ENat.coe_toNat + by_contra C + rw [(h₁f u hu).order_eq_top_iff] at C + rw [← (h₁f u hu).frequently_zero_iff_eventually_zero] at C + obtain ⟨u₁, h₁u₁, h₂u₁⟩ := h₂f + rw [(h₁f.eqOn_zero_of_preconnected_of_frequently_eq_zero hU hu C) h₁u₁] at h₂u₁ + tauto + + +theorem discreteZeros + {f : ℂ → ℂ} + {U : Set ℂ} + (hU : IsPreconnected U) + (h₁f : AnalyticOn ℂ f U) + (h₂f : ∃ u ∈ U, f u ≠ 0) : + DiscreteTopology ↑(U ∩ f⁻¹' {0}) := by + + simp_rw [← singletons_open_iff_discrete] + simp_rw [Metric.isOpen_singleton_iff] + + intro z + + let A := XX hU h₁f h₂f z.2.1 + rw [eq_comm] at A + rw [AnalyticAt.order_eq_nat_iff] at A + obtain ⟨g, h₁g, h₂g, h₃g⟩ := A + + rw [Metric.eventually_nhds_iff_ball] at h₃g + have : ∃ ε > 0, ∀ y ∈ Metric.ball (↑z) ε, g y ≠ 0 := by + have h₄g : ContinuousAt g z := AnalyticAt.continuousAt h₁g + have : {0}ᶜ ∈ nhds (g z) := by + exact compl_singleton_mem_nhds_iff.mpr h₂g + + let F := h₄g.preimage_mem_nhds this + rw [Metric.mem_nhds_iff] at F + obtain ⟨ε, h₁ε, h₂ε⟩ := F + use ε + constructor; exact h₁ε + intro y hy + let G := h₂ε hy + simp at G + exact G + obtain ⟨ε₁, h₁ε₁⟩ := this + + obtain ⟨ε₂, h₁ε₂, h₂ε₂⟩ := h₃g + use min ε₁ ε₂ + constructor + · have : 0 < min ε₁ ε₂ := by + rw [lt_min_iff] + exact And.imp_right (fun _ => h₁ε₂) h₁ε₁ + exact this + + intro y + intro h₁y + + have h₂y : ↑y ∈ Metric.ball (↑z) ε₂ := by + simp + calc dist y z + _ < min ε₁ ε₂ := by assumption + _ ≤ ε₂ := by exact min_le_right ε₁ ε₂ + + have h₃y : ↑y ∈ Metric.ball (↑z) ε₁ := by + simp + calc dist y z + _ < min ε₁ ε₂ := by assumption + _ ≤ ε₁ := by exact min_le_left ε₁ ε₂ + + + have F := h₂ε₂ y.1 h₂y + rw [y.2.2] at F + simp at F + + have : g y.1 ≠ 0 := by + exact h₁ε₁.2 y h₃y + simp [this] at F + ext + rw [sub_eq_zero] at F + tauto + + +theorem finiteZeros + {f : ℂ → ℂ} + {U : Set ℂ} + (h₁U : IsPreconnected U) + (h₂U : IsCompact U) + (h₁f : AnalyticOn ℂ f U) + (h₂f : ∃ u ∈ U, f u ≠ 0) : + Set.Finite ↑(U ∩ f⁻¹' {0}) := by + + have hinter : IsCompact ↑(U ∩ f⁻¹' {0}) := by + apply IsCompact.of_isClosed_subset h₂U + apply h₁f.continuousOn.preimage_isClosed_of_isClosed + exact IsCompact.isClosed h₂U + exact isClosed_singleton + exact Set.inter_subset_left + + apply hinter.finite + apply DiscreteTopology.of_subset (s := ↑(U ∩ f⁻¹' {0})) + exact discreteZeros h₁U h₁f h₂f + rfl + + +theorem AnalyticOnCompact.eliminateZeros + {f : ℂ → ℂ} + {U : Set ℂ} + (h₁U : IsPreconnected U) + (h₂U : IsCompact U) + (h₁f : AnalyticOn ℂ f U) + (h₂f : ∃ u ∈ U, f u ≠ 0) : + ∃ (g : ℂ → ℂ) (A : Finset U), AnalyticOn ℂ g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (h₁f a a.2).order.toNat) • g z := by + + let ι : U → ℂ := Subtype.val + + let A₁ := ι⁻¹' (U ∩ f⁻¹' {0}) + + have : A₁.Finite := by + apply Set.Finite.preimage + exact Set.injOn_subtype_val + exact finiteZeros h₁U h₂U h₁f h₂f + let A := this.toFinset + + let n : ℂ → ℕ := by + intro z + by_cases hz : z ∈ U + · exact (h₁f z hz).order.toNat + · exact 0 + + have hn : ∀ a ∈ A, (h₁f a a.2).order = n a := by + intro a _ + dsimp [n] + simp + rw [eq_comm] + apply XX h₁U + exact h₂f + + obtain ⟨g, h₁g, h₂g, h₃g⟩ := AnalyticOn.eliminateZeros (A := A) h₁f n hn + use g + use A + + have inter : ∀ (z : ℂ), f z = (∏ a ∈ A, (z - ↑a) ^ (h₁f (↑a) a.property).order.toNat) • g z := by + intro z + rw [h₃g z] + congr + funext a + congr + dsimp [n] + simp [a.2] + + constructor + · exact h₁g + · constructor + · intro z h₁z + by_cases h₂z : ⟨z, h₁z⟩ ∈ ↑A.toSet + · exact h₂g ⟨z, h₁z⟩ h₂z + · have : f z ≠ 0 := by + by_contra C + have : ⟨z, h₁z⟩ ∈ ↑A₁ := by + dsimp [A₁, ι] + simp + exact C + have : ⟨z, h₁z⟩ ∈ ↑A.toSet := by + dsimp [A] + simp + exact this + tauto + rw [inter z] at this + exact right_ne_zero_of_smul this + · exact inter + + +noncomputable def AnalyticOn.order + {f : ℂ → ℂ} + {U : Set ℂ} + (hf : AnalyticOn ℂ f U) : + ℂ → ℕ∞ := by + intro z + if hz : z ∈ U then + exact (hf z hz).order + else + exact 0 + + +theorem AnalyticOnCompact.eliminateZeros₁ + {f : ℂ → ℂ} + {U : Set ℂ} + (h₁U : IsPreconnected U) + (h₂U : IsCompact U) + (h₁f : AnalyticOn ℂ f U) + (h₂f : ∃ u ∈ U, f u ≠ 0) : + ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ᶠ u, (z - u) ^ (h₁f.order u).toNat) • g z := by + + obtain ⟨g, A, h₁g, h₂g, h₃g⟩ := AnalyticOnCompact.eliminateZeros h₁U h₂U h₁f h₂f + + use g + constructor + · exact h₁g + · constructor + · exact h₂g + · intro z + rw [h₃g z] + congr + + sorry diff --git a/Nevanlinna/laplace.lean b/Nevanlinna/laplace.lean index 35c1128..d85b4d0 100644 --- a/Nevanlinna/laplace.lean +++ b/Nevanlinna/laplace.lean @@ -85,11 +85,11 @@ theorem laplace_add_ContDiffOn have t₁ : DifferentiableAt ℝ (partialDeriv ℝ 1 f₁) x := by let B₀ := (h₁ x hx).contDiffAt (IsOpen.mem_nhds hs hx) let A₀ := partialDeriv_contDiffAt ℝ B₀ 1 - exact A₀.differentiableAt (Submonoid.oneLE.proof_2 ℕ∞) + apply A₀.differentiableAt (Preorder.le_refl 1) have t₂ : DifferentiableAt ℝ (partialDeriv ℝ 1 f₂) x := by let B₀ := (h₂ x hx).contDiffAt (IsOpen.mem_nhds hs hx) let A₀ := partialDeriv_contDiffAt ℝ B₀ 1 - exact A₀.differentiableAt (Submonoid.oneLE.proof_2 ℕ∞) + exact A₀.differentiableAt (Preorder.le_refl 1) rw [partialDeriv_add₂_differentiableAt ℝ t₁ t₂] have : partialDeriv ℝ Complex.I (f₁ + f₂) =ᶠ[nhds x] (partialDeriv ℝ Complex.I f₁) + (partialDeriv ℝ Complex.I f₂) := by @@ -105,11 +105,11 @@ theorem laplace_add_ContDiffOn have t₃ : DifferentiableAt ℝ (partialDeriv ℝ Complex.I f₁) x := by let B₀ := (h₁ x hx).contDiffAt (IsOpen.mem_nhds hs hx) let A₀ := partialDeriv_contDiffAt ℝ B₀ Complex.I - exact A₀.differentiableAt (Submonoid.oneLE.proof_2 ℕ∞) + exact A₀.differentiableAt (Preorder.le_refl 1) have t₄ : DifferentiableAt ℝ (partialDeriv ℝ Complex.I f₂) x := by let B₀ := (h₂ x hx).contDiffAt (IsOpen.mem_nhds hs hx) let A₀ := partialDeriv_contDiffAt ℝ B₀ Complex.I - exact A₀.differentiableAt (Submonoid.oneLE.proof_2 ℕ∞) + exact A₀.differentiableAt (Preorder.le_refl 1) rw [partialDeriv_add₂_differentiableAt ℝ t₃ t₄] -- I am super confused at this point because the tactic 'ring' does not work. diff --git a/Nevanlinna/periodic_integrability.lean b/Nevanlinna/periodic_integrability.lean index bd382dd..d55165d 100644 --- a/Nevanlinna/periodic_integrability.lean +++ b/Nevanlinna/periodic_integrability.lean @@ -76,7 +76,7 @@ theorem periodic_integrability4 obtain ⟨n₁, hn₁⟩ := exists_nat_ge ((t -min a₁ a₂) / T) use n₁ rw [sub_le_iff_le_add] - rw [div_le_iff hT] at hn₁ + rw [div_le_iff₀ hT] at hn₁ rw [sub_le_iff_le_add] at hn₁ rw [add_comm] exact hn₁ @@ -84,7 +84,7 @@ theorem periodic_integrability4 obtain ⟨n₂, hn₂⟩ := exists_nat_ge ((max a₁ a₂ - t) / T) use n₂ rw [← sub_le_iff_le_add] - rw [div_le_iff hT] at hn₂ + rw [div_le_iff₀ hT] at hn₂ linarith have : Set.uIcc a₁ a₂ ⊆ Set.uIcc (t - n₁ * T) (t + n₂ * T) := by diff --git a/Nevanlinna/specialFunctions_Integral_log_sin.lean b/Nevanlinna/specialFunctions_Integral_log_sin.lean index ca37f2f..e70488b 100644 --- a/Nevanlinna/specialFunctions_Integral_log_sin.lean +++ b/Nevanlinna/specialFunctions_Integral_log_sin.lean @@ -1,5 +1,6 @@ import Mathlib.Analysis.SpecialFunctions.Integrals import Mathlib.Analysis.SpecialFunctions.Log.NegMulLog +import Mathlib.Analysis.Convex.SpecificFunctions.Deriv open scoped Interval Topology open Real Filter MeasureTheory intervalIntegral