From 6329e081a345d030d33e6aa4350ab9b04e02448b Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Fri, 3 Jan 2025 18:08:55 +0100 Subject: [PATCH] Add leftovers --- .../leftovers/analyticOnNhd_divisor.lean | 59 +++ .../leftovers/analyticOnNhd_zeroSet.lean | 461 ++++++++++++++++++ Nevanlinna/leftovers/bilinear.lean | 77 +++ Nevanlinna/leftovers/diffOp.lean | 104 ++++ Nevanlinna/leftovers/holomorphic.lean | 176 +++++++ Nevanlinna/leftovers/holomorphic_zero.lean | 171 +++++++ .../specialFunctions_Integral_log.lean | 65 +++ 7 files changed, 1113 insertions(+) create mode 100644 Nevanlinna/leftovers/analyticOnNhd_divisor.lean create mode 100644 Nevanlinna/leftovers/analyticOnNhd_zeroSet.lean create mode 100644 Nevanlinna/leftovers/bilinear.lean create mode 100644 Nevanlinna/leftovers/diffOp.lean create mode 100644 Nevanlinna/leftovers/holomorphic.lean create mode 100644 Nevanlinna/leftovers/holomorphic_zero.lean create mode 100644 Nevanlinna/leftovers/specialFunctions_Integral_log.lean diff --git a/Nevanlinna/leftovers/analyticOnNhd_divisor.lean b/Nevanlinna/leftovers/analyticOnNhd_divisor.lean new file mode 100644 index 0000000..a7a2623 --- /dev/null +++ b/Nevanlinna/leftovers/analyticOnNhd_divisor.lean @@ -0,0 +1,59 @@ +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 diff --git a/Nevanlinna/leftovers/analyticOnNhd_zeroSet.lean b/Nevanlinna/leftovers/analyticOnNhd_zeroSet.lean new file mode 100644 index 0000000..df14a9d --- /dev/null +++ b/Nevanlinna/leftovers/analyticOnNhd_zeroSet.lean @@ -0,0 +1,461 @@ +import Mathlib.Analysis.Analytic.Constructions +import Mathlib.Analysis.Analytic.IsolatedZeros +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 + + +theorem AnalyticOnNhd.order_eq_nat_iff + {f : ℂ → ℂ} + {U : Set ℂ} + {z₀ : U} + (hf : AnalyticOnNhd ℂ f U) + (n : ℕ) : + hf.order z₀ = ↑n ↔ ∃ (g : ℂ → ℂ), AnalyticOnNhd ℂ 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₀ z₀.2) 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₀.1}ᶜ + 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 + dsimp [AnalyticOnNhd.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₁ + {f : ℂ → ℂ} + {U : Set ℂ} + (hf : AnalyticOnNhd ℂ f U) : + Function.support hf.order = U.restrict f⁻¹' {0} := by + ext u + simp [AnalyticOnNhd.order] + rw [not_iff_comm, (hf u u.2).order_eq_zero_iff] + + +theorem AnalyticOnNhd.eliminateZeros + {f : ℂ → ℂ} + {U : Set ℂ} + {A : Finset U} + (hf : AnalyticOnNhd ℂ 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 + + 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) + + -- 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) + + 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₁⟩ := (AnalyticOnNhd.order_eq_nat_iff h₁g₀ (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 : AnalyticOnNhd ℂ 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 : AnalyticOnNhd ℂ f U) + (h₂f : ∃ u ∈ U, f u ≠ 0) : + DiscreteTopology ((U.restrict 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.1.2 + 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 + have : f y = 0 := by exact y.2 + rw [this] 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 : AnalyticOnNhd ℂ f U) + (h₂f : ∃ u ∈ U, f u ≠ 0) : + Set.Finite (U.restrict f⁻¹' {0}) := by + + have closedness : IsClosed (U.restrict f⁻¹' {0}) := by + apply IsClosed.preimage + apply continuousOn_iff_continuous_restrict.1 + exact h₁f.continuousOn + exact isClosed_singleton + + have : CompactSpace U := by + exact isCompact_iff_compactSpace.mp h₂U + + apply (IsClosed.isCompact closedness).finite + exact discreteZeros h₁U h₁f h₂f + + +theorem AnalyticOnNhdCompact.eliminateZeros + {f : ℂ → ℂ} + {U : Set ℂ} + (h₁U : IsPreconnected U) + (h₂U : IsCompact U) + (h₁f : AnalyticOnNhd ℂ 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 + + let A := (finiteZeros h₁U h₂U h₁f h₂f).toFinset + + let n : U → ℕ := fun z ↦ (h₁f z z.2).order.toNat + + have hn : ∀ a ∈ A, (h₁f a a.2).order = n a := by + intro a _ + dsimp [n, AnalyticOnNhd.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 + 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] + + 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.toSet := by + dsimp [A] + simp + exact C + tauto + rw [inter z] at this + exact right_ne_zero_of_smul this + · exact inter + + +theorem AnalyticOnNhdCompact.eliminateZeros₂ + {f : ℂ → ℂ} + {U : Set ℂ} + (h₁U : IsPreconnected U) + (h₂U : IsCompact U) + (h₁f : AnalyticOnNhd ℂ 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 + + let A := (finiteZeros h₁U h₂U h₁f h₂f).toFinset + + let n : U → ℕ := fun z ↦ (h₁f z z.2).order.toNat + + have hn : ∀ a ∈ A, (h₁f a a.2).order = n a := by + intro a _ + dsimp [n, AnalyticOnNhd.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 + use g + + 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] + + 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.toSet := by + dsimp [A] + simp + exact C + tauto + rw [inter z] at this + exact right_ne_zero_of_smul this + · exact h₃g + + +theorem AnalyticOnNhdCompact.eliminateZeros₁ + {f : ℂ → ℂ} + {U : Set ℂ} + (h₁U : IsPreconnected U) + (h₂U : IsCompact U) + (h₁f : AnalyticOnNhd ℂ 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 + + let A := (finiteZeros h₁U h₂U h₁f h₂f).toFinset + + let n : U → ℕ := fun z ↦ (h₁f z z.2).order.toNat + + have hn : ∀ a ∈ A, (h₁f a a.2).order = n a := by + intro a _ + dsimp [n, AnalyticOnNhd.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 + use g + + 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] + + 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.toSet := by + dsimp [A] + simp + exact C + tauto + rw [inter z] at this + exact right_ne_zero_of_smul this + · intro z + + let φ : U → ℂ := fun a ↦ (z - ↑a) ^ (h₁f.order a).toNat + have hφ : Function.mulSupport φ ⊆ A := by + intro x hx + simp [φ] at hx + have : (h₁f.order x).toNat ≠ 0 := by + by_contra C + rw [C] at hx + simp at hx + simp [A] + exact AnalyticAt.supp_order_toNat (h₁f x x.2) this + rw [finprod_eq_prod_of_mulSupport_subset φ hφ] + rw [inter z] + rfl diff --git a/Nevanlinna/leftovers/bilinear.lean b/Nevanlinna/leftovers/bilinear.lean new file mode 100644 index 0000000..533b209 --- /dev/null +++ b/Nevanlinna/leftovers/bilinear.lean @@ -0,0 +1,77 @@ +/- +Copyright (c) 2024 Stefan Kebekus. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Stefan Kebekus +-/ + +import Mathlib.Analysis.InnerProductSpace.PiL2 + +/-! + +# Canoncial Elements in Tensor Powers of Real Inner Product Spaces + +Given an `InnerProductSpace ℝ E`, this file defines two canonical tensors, which +are relevant when for a coordinate-free definition of differential operators +such as the Laplacian. + +* `InnerProductSpace.canonicalContravariantTensor E : E ⊗[ℝ] E →ₗ[ℝ] ℝ`. This is + the element corresponding to the inner product. + +* If `E` is finite-dimensional, then `E ⊗[ℝ] E` is canonically isomorphic to its + dual. Accordingly, there exists an element + `InnerProductSpace.canonicalCovariantTensor E : E ⊗[ℝ] E` that corresponds to + `InnerProductSpace.canonicalContravariantTensor E` under this identification. + +The theorem `InnerProductSpace.canonicalCovariantTensorRepresentation` shows +that `InnerProductSpace.canonicalCovariantTensor E` can be computed from any +orthonormal basis `v` as `∑ i, (v i) ⊗ₜ[ℝ] (v i)`. + +-/ + +open InnerProductSpace +open TensorProduct + + +noncomputable def InnerProductSpace.canonicalContravariantTensor + {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] + : E ⊗[ℝ] E →ₗ[ℝ] ℝ := TensorProduct.lift bilinFormOfRealInner + + +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 + + let w := stdOrthonormalBasis ℝ E + conv => + right + arg 2 + intro i + rw [← w.sum_repr' (v i)] + simp_rw [TensorProduct.sum_tmul, TensorProduct.tmul_sum, TensorProduct.smul_tmul_smul] + + conv => + right + rw [Finset.sum_comm] + arg 2 + intro y + rw [Finset.sum_comm] + arg 2 + intro x + rw [← Finset.sum_smul] + arg 1 + arg 2 + intro i + rw [← real_inner_comm (w x)] + simp_rw [OrthonormalBasis.sum_inner_mul_inner v] + + have {i} : ∑ j, ⟪w i, w j⟫_ℝ • w i ⊗ₜ[ℝ] w j = w i ⊗ₜ[ℝ] w i := by + rw [Fintype.sum_eq_single i, orthonormal_iff_ite.1 w.orthonormal]; simp + intro _ _; rw [orthonormal_iff_ite.1 w.orthonormal]; simp; tauto + simp_rw [this] + rfl diff --git a/Nevanlinna/leftovers/diffOp.lean b/Nevanlinna/leftovers/diffOp.lean new file mode 100644 index 0000000..3b161fe --- /dev/null +++ b/Nevanlinna/leftovers/diffOp.lean @@ -0,0 +1,104 @@ +import Mathlib.Analysis.Calculus.ContDiff.Basic +import Mathlib.Analysis.InnerProductSpace.PiL2 + +/- + +Let E, F, G be vector spaces over nontrivally normed field 𝕜, a homogeneus +linear differential operator of order n is a map that attaches to every point e +of E a linear evaluation + +{Continuous 𝕜-multilinear maps E → F in n variables} → G + +In other words, homogeneus linear differential operator of order n is an +instance of the type: + +D : E → (ContinuousMultilinearMap 𝕜 (fun _ : Fin n ↦ E) F) →ₗ[𝕜] G + +Given any map f : E → F, one obtains a map D f : E → G by sending a point e to +the evaluation (D e), applied to the n.th derivative of f at e + +fun e ↦ D e (iteratedFDeriv 𝕜 n f e) + +-/ + +@[ext] +class HomLinDiffOp + (𝕜 : Type*) [NontriviallyNormedField 𝕜] + (n : ℕ) + (E : Type*) [NormedAddCommGroup E] [NormedSpace 𝕜 E] + (F : Type*) [NormedAddCommGroup F] [NormedSpace 𝕜 F] + (G : Type*) [NormedAddCommGroup G] [NormedSpace 𝕜 G] +where + tensorfield : E → ( E [×n]→L[𝕜] F) →L[𝕜] G +-- tensorfield : E → (ContinuousMultilinearMap 𝕜 (fun _ : Fin n ↦ E) F) →ₗ[𝕜] G + + +namespace HomLinDiffOp + +noncomputable def toFun + {𝕜 : Type*} [NontriviallyNormedField 𝕜] + {n : ℕ} + {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] + {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F] + {G : Type*} [NormedAddCommGroup G] [NormedSpace 𝕜 G] + (o : HomLinDiffOp 𝕜 n E F G) + : (E → F) → (E → G) := + fun f z ↦ o.tensorfield z (iteratedFDeriv 𝕜 n f z) + + +noncomputable def Laplace + {𝕜 : Type*} [RCLike 𝕜] + {n : ℕ} + : HomLinDiffOp 𝕜 2 (EuclideanSpace 𝕜 (Fin n)) 𝕜 𝕜 + where + tensorfield := by + intro _ + + let v := stdOrthonormalBasis 𝕜 (EuclideanSpace 𝕜 (Fin n)) + rw [finrank_euclideanSpace_fin] at v + + exact { + toFun := fun f' ↦ ∑ i, f' ![v i, v i] + map_add' := by + intro f₁ f₂ + exact Finset.sum_add_distrib + map_smul' := by + intro m f + exact Eq.symm (Finset.mul_sum Finset.univ (fun i ↦ f ![v i, v i]) m) + cont := by + simp + apply continuous_finset_sum + intro i _ + exact ContinuousEvalConst.continuous_eval_const ![v i, v i] + } + + +noncomputable def Gradient + {𝕜 : Type*} [RCLike 𝕜] + {n : ℕ} + : HomLinDiffOp 𝕜 1 (EuclideanSpace 𝕜 (Fin n)) 𝕜 (EuclideanSpace 𝕜 (Fin n)) + where + tensorfield := by + intro _ + + let v := stdOrthonormalBasis 𝕜 (EuclideanSpace 𝕜 (Fin n)) + rw [finrank_euclideanSpace_fin] at v + + exact { + toFun := fun f' ↦ ∑ i, (f' ![v i]) • (v i) + map_add' := by + intro f₁ f₂ + simp; simp_rw [add_smul, Finset.sum_add_distrib] + map_smul' := by + intro m f + simp; simp_rw [Finset.smul_sum, ←smul_assoc,smul_eq_mul] + cont := by + simp + apply continuous_finset_sum + intro i _ + apply Continuous.smul + exact ContinuousEvalConst.continuous_eval_const ![v i] + exact continuous_const + } + +end HomLinDiffOp diff --git a/Nevanlinna/leftovers/holomorphic.lean b/Nevanlinna/leftovers/holomorphic.lean new file mode 100644 index 0000000..93e6672 --- /dev/null +++ b/Nevanlinna/leftovers/holomorphic.lean @@ -0,0 +1,176 @@ +import Mathlib.Analysis.Complex.TaylorSeries +import Nevanlinna.cauchyRiemann + +variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] +variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] +variable {G : Type*} [NormedAddCommGroup G] [NormedSpace ℂ G] + +def HolomorphicAt (f : E → F) (x : E) : Prop := + ∃ s ∈ nhds x, ∀ z ∈ s, DifferentiableAt ℂ f z + + +theorem HolomorphicAt_iff + {f : E → F} + {x : E} : + HolomorphicAt f x ↔ ∃ s : + Set E, IsOpen s ∧ x ∈ s ∧ (∀ z ∈ s, DifferentiableAt ℂ f z) := by + constructor + · intro hf + obtain ⟨t, h₁t, h₂t⟩ := hf + obtain ⟨s, h₁s, h₂s, h₃s⟩ := mem_nhds_iff.1 h₁t + use s + constructor + · assumption + · constructor + · assumption + · intro z hz + exact h₂t z (h₁s hz) + · intro hyp + obtain ⟨s, h₁s, h₂s, hf⟩ := hyp + use s + constructor + · apply (IsOpen.mem_nhds_iff h₁s).2 h₂s + · assumption + + +theorem HolomorphicAt_analyticAt + [CompleteSpace F] + {f : ℂ → F} + {x : ℂ} : + HolomorphicAt f x → AnalyticAt ℂ f x := by + intro hf + obtain ⟨s, h₁s, h₂s, h₃s⟩ := HolomorphicAt_iff.1 hf + apply DifferentiableOn.analyticAt (s := s) + intro z hz + apply DifferentiableAt.differentiableWithinAt + apply h₃s + exact hz + exact IsOpen.mem_nhds h₁s h₂s + + +theorem HolomorphicAt_differentiableAt + {f : E → F} + {x : E} : + HolomorphicAt f x → DifferentiableAt ℂ f x := by + intro hf + obtain ⟨s, _, h₂s, h₃s⟩ := HolomorphicAt_iff.1 hf + exact h₃s x h₂s + + +theorem HolomorphicAt_isOpen + (f : E → F) : + IsOpen { x : E | HolomorphicAt f x } := by + + rw [← subset_interior_iff_isOpen] + intro x hx + simp at hx + obtain ⟨s, h₁s, h₂s, h₃s⟩ := HolomorphicAt_iff.1 hx + use s + constructor + · simp + constructor + · exact h₁s + · intro x hx + simp + use s + constructor + · exact IsOpen.mem_nhds h₁s hx + · exact h₃s + · exact h₂s + + +theorem HolomorphicAt_comp + {g : E → F} + {f : F → G} + {z : E} + (hf : HolomorphicAt f (g z)) + (hg : HolomorphicAt g z) : + HolomorphicAt (f ∘ g) z := by + obtain ⟨UE, h₁UE, h₂UE⟩ := hg + obtain ⟨UF, h₁UF, h₂UF⟩ := hf + use UE ∩ g⁻¹' UF + constructor + · simp + constructor + · assumption + · apply ContinuousAt.preimage_mem_nhds + apply (h₂UE z (mem_of_mem_nhds h₁UE)).continuousAt + assumption + · intro x hx + apply DifferentiableAt.comp + apply h₂UF + exact hx.2 + apply h₂UE + exact hx.1 + + +theorem HolomorphicAt_neg + {f : E → F} + {z : E} + (hf : HolomorphicAt f z) : + HolomorphicAt (-f) z := by + obtain ⟨UF, h₁UF, h₂UF⟩ := hf + use UF + constructor + · assumption + · intro z hz + apply differentiableAt_neg_iff.mp + simp + exact h₂UF z hz + + +theorem HolomorphicAt_contDiffAt + [CompleteSpace F] + {f : ℂ → F} + {z : ℂ} + (hf : HolomorphicAt f z) : + ContDiffAt ℝ 2 f z := by + + let t := {x | HolomorphicAt f x} + have ht : IsOpen t := HolomorphicAt_isOpen f + have hz : z ∈ t := by exact hf + + -- ContDiffAt ℝ 2 f z + apply ContDiffOn.contDiffAt _ ((IsOpen.mem_nhds_iff ht).2 hz) + suffices h : ContDiffOn ℂ 2 f t from by + apply ContDiffOn.restrict_scalars ℝ h + apply DifferentiableOn.contDiffOn _ ht + intro w hw + apply DifferentiableAt.differentiableWithinAt + exact HolomorphicAt_differentiableAt hw + + +theorem CauchyRiemann'₅ + {f : ℂ → F} + {z : ℂ} + (h : DifferentiableAt ℂ f z) : + partialDeriv ℝ Complex.I f z = Complex.I • partialDeriv ℝ 1 f z := by + unfold partialDeriv + + conv => + left + rw [DifferentiableAt.fderiv_restrictScalars ℝ h] + simp + rw [← mul_one Complex.I] + rw [← smul_eq_mul] + conv => + right + right + rw [DifferentiableAt.fderiv_restrictScalars ℝ h] + simp + +theorem CauchyRiemann'₆ + {f : ℂ → F} + {z : ℂ} + (h : HolomorphicAt f z) : + partialDeriv ℝ Complex.I f =ᶠ[nhds z] Complex.I • partialDeriv ℝ 1 f := by + + obtain ⟨s, h₁s, hz, h₂f⟩ := HolomorphicAt_iff.1 h + + apply Filter.eventuallyEq_iff_exists_mem.2 + use s + constructor + · exact IsOpen.mem_nhds h₁s hz + · intro w hw + apply CauchyRiemann'₅ + exact h₂f w hw diff --git a/Nevanlinna/leftovers/holomorphic_zero.lean b/Nevanlinna/leftovers/holomorphic_zero.lean new file mode 100644 index 0000000..55879bf --- /dev/null +++ b/Nevanlinna/leftovers/holomorphic_zero.lean @@ -0,0 +1,171 @@ +import Init.Classical +import Mathlib.Analysis.Analytic.Meromorphic +import Mathlib.Topology.ContinuousOn +import Mathlib.Analysis.Analytic.IsolatedZeros +import Nevanlinna.leftovers.holomorphic +import Nevanlinna.leftovers.analyticOnNhd_zeroSet + + +noncomputable def zeroDivisor + (f : ℂ → ℂ) : + ℂ → ℕ := by + intro z + by_cases hf : AnalyticAt ℂ f z + · exact hf.order.toNat + · exact 0 + + +theorem analyticAtZeroDivisorSupport + {f : ℂ → ℂ} + {z : ℂ} + (h : z ∈ Function.support (zeroDivisor f)) : + AnalyticAt ℂ f z := by + + by_contra h₁f + simp at h + dsimp [zeroDivisor] at h + simp [h₁f] at h + + +theorem zeroDivisor_eq_ord_AtZeroDivisorSupport + {f : ℂ → ℂ} + {z : ℂ} + (h : z ∈ Function.support (zeroDivisor f)) : + zeroDivisor f z = (analyticAtZeroDivisorSupport h).order.toNat := by + + unfold zeroDivisor + simp [analyticAtZeroDivisorSupport h] + + + +lemma toNatEqSelf_iff {n : ℕ∞} : n.toNat = n ↔ ∃ m : ℕ, m = n := by + constructor + · intro H₁ + rw [← ENat.some_eq_coe, ← WithTop.ne_top_iff_exists] + by_contra H₂ + rw [H₂] at H₁ + simp at H₁ + · intro H + obtain ⟨m, hm⟩ := H + rw [← hm] + simp + + +lemma natural_if_toNatNeZero {n : ℕ∞} : n.toNat ≠ 0 → ∃ m : ℕ, m = n := by + rw [← ENat.some_eq_coe, ← WithTop.ne_top_iff_exists] + contrapose; simp; tauto + + +theorem zeroDivisor_localDescription + {f : ℂ → ℂ} + {z₀ : ℂ} + (h : z₀ ∈ Function.support (zeroDivisor f)) : + ∃ (g : ℂ → ℂ), AnalyticAt ℂ g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds z₀, f z = (z - z₀) ^ (zeroDivisor f z₀) • g z := by + + have A : zeroDivisor f ↑z₀ ≠ 0 := by exact h + let B := zeroDivisor_eq_ord_AtZeroDivisorSupport h + rw [B] at A + have C := natural_if_toNatNeZero A + obtain ⟨m, hm⟩ := C + have h₂m : m ≠ 0 := by + rw [← hm] at A + simp at A + assumption + rw [eq_comm] at hm + let E := AnalyticAt.order_eq_nat_iff (analyticAtZeroDivisorSupport h) m + let F := hm + rw [E] at F + + have : m = zeroDivisor f z₀ := by + rw [B, hm] + simp + rwa [this] at F + + +theorem zeroDivisor_zeroSet + {f : ℂ → ℂ} + {z₀ : ℂ} + (h : z₀ ∈ Function.support (zeroDivisor f)) : + f z₀ = 0 := by + obtain ⟨g, _, _, h₃⟩ := zeroDivisor_localDescription h + rw [Filter.Eventually.self_of_nhds h₃] + simp + left + exact h + + +theorem zeroDivisor_support_iff + {f : ℂ → ℂ} + {z₀ : ℂ} : + z₀ ∈ Function.support (zeroDivisor f) ↔ + f z₀ = 0 ∧ + AnalyticAt ℂ f z₀ ∧ + ∃ (g : ℂ → ℂ), AnalyticAt ℂ g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds z₀, f z = (z - z₀) ^ (zeroDivisor f z₀) • g z := by + constructor + · intro hz + constructor + · exact zeroDivisor_zeroSet hz + · constructor + · exact analyticAtZeroDivisorSupport hz + · exact zeroDivisor_localDescription hz + · intro ⟨h₁, h₂, h₃⟩ + have : zeroDivisor f z₀ = (h₂.order).toNat := by + unfold zeroDivisor + simp [h₂] + simp [this] + simp [(h₂.order_eq_nat_iff (zeroDivisor f z₀)).2 h₃] + obtain ⟨g, h₁g, h₂g, h₃g⟩ := h₃ + rw [Filter.Eventually.self_of_nhds h₃g] at h₁ + simp [h₂g] at h₁ + assumption + + +theorem topOnPreconnected + {f : ℂ → ℂ} + {U : Set ℂ} + (hU : IsPreconnected U) + (h₁f : AnalyticOnNhd ℂ f U) + (h₂f : ∃ z ∈ U, f z ≠ 0) : + ∀ (hz : z ∈ U), (h₁f z hz).order ≠ ⊤ := by + + by_contra H + push_neg at H + 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' + tauto + + +theorem supportZeroSet + {f : ℂ → ℂ} + {U : Set ℂ} + (hU : IsPreconnected U) + (h₁f : AnalyticOnNhd ℂ f U) + (h₂f : ∃ z ∈ U, f z ≠ 0) : + U ∩ Function.support (zeroDivisor f) = U ∩ f⁻¹' {0} := by + + ext x + constructor + · intro hx + constructor + · exact hx.1 + exact zeroDivisor_zeroSet hx.2 + · simp + intro h₁x h₂x + constructor + · exact h₁x + · let A := zeroDivisor_support_iff (f := f) (z₀ := x) + simp at A + rw [A] + constructor + · exact h₂x + · constructor + · exact h₁f x h₁x + · have B := AnalyticAt.order_eq_nat_iff (h₁f x h₁x) (zeroDivisor f x) + simp at B + rw [← B] + dsimp [zeroDivisor] + simp [h₁f x h₁x] + refine Eq.symm (ENat.coe_toNat ?h.mpr.right.right.right.a) + exact topOnPreconnected hU h₁f h₂f h₁x diff --git a/Nevanlinna/leftovers/specialFunctions_Integral_log.lean b/Nevanlinna/leftovers/specialFunctions_Integral_log.lean new file mode 100644 index 0000000..9b8eaae --- /dev/null +++ b/Nevanlinna/leftovers/specialFunctions_Integral_log.lean @@ -0,0 +1,65 @@ +import Mathlib.Analysis.SpecialFunctions.Integrals +import Mathlib.Analysis.SpecialFunctions.Log.NegMulLog +import Mathlib.MeasureTheory.Integral.CircleIntegral +import Mathlib.MeasureTheory.Measure.Restrict + +open scoped Interval Topology +open Real Filter MeasureTheory intervalIntegral + +-- The following theorem was suggested by Gareth Ma on Zulip + + +theorem logInt + {t : ℝ} + (ht : 0 < t) : + ∫ x in (0 : ℝ)..t, log x = t * log t - t := by + rw [← integral_add_adjacent_intervals (b := 1)] + trans (-1) + (t * log t - t + 1) + · congr + · -- ∫ x in 0..1, log x = -1, same proof as before + rw [integral_eq_sub_of_hasDerivAt_of_tendsto (f := fun x ↦ x * log x - x) (fa := 0) (fb := -1)] + · simp + · simp + · intro x hx + norm_num at hx + convert (hasDerivAt_mul_log hx.left.ne.symm).sub (hasDerivAt_id x) using 1 + norm_num + · rw [← neg_neg log] + apply IntervalIntegrable.neg + apply intervalIntegrable_deriv_of_nonneg (g := fun x ↦ -(x * log x - x)) + · exact (continuous_mul_log.continuousOn.sub continuous_id.continuousOn).neg + · intro x hx + norm_num at hx + convert ((hasDerivAt_mul_log hx.left.ne.symm).sub (hasDerivAt_id x)).neg using 1 + norm_num + · intro x hx + norm_num at hx + rw [Pi.neg_apply, Left.nonneg_neg_iff] + exact (log_nonpos_iff hx.left).mpr hx.right.le + · have := tendsto_log_mul_rpow_nhds_zero zero_lt_one + simp_rw [rpow_one, mul_comm] at this + -- tendsto_nhdsWithin_of_tendsto_nhds should be under Tendsto namespace + convert this.sub (tendsto_nhdsWithin_of_tendsto_nhds tendsto_id) + norm_num + · rw [(by simp : -1 = 1 * log 1 - 1)] + apply tendsto_nhdsWithin_of_tendsto_nhds + exact (continuousAt_id.mul (continuousAt_log one_ne_zero)).sub continuousAt_id + · -- ∫ x in 1..t, log x = t * log t + 1, just use integral_log_of_pos + rw [integral_log_of_pos zero_lt_one ht] + norm_num + · abel + · -- log is integrable on [[0, 1]] + rw [← neg_neg log] + apply IntervalIntegrable.neg + apply intervalIntegrable_deriv_of_nonneg (g := fun x ↦ -(x * log x - x)) + · exact (continuous_mul_log.continuousOn.sub continuous_id.continuousOn).neg + · intro x hx + norm_num at hx + convert ((hasDerivAt_mul_log hx.left.ne.symm).sub (hasDerivAt_id x)).neg using 1 + norm_num + · intro x hx + norm_num at hx + rw [Pi.neg_apply, Left.nonneg_neg_iff] + exact (log_nonpos_iff hx.left).mpr hx.right.le + · -- log is integrable on [[0, t]] + simp [Set.mem_uIcc, ht]