Add leftovers

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

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

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

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

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

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

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]