Nevanlinna/analyticAt.lean

@@ -1,238 +0,0 @@
-import Mathlib.Analysis.Analytic.IsolatedZeros
-import Mathlib.Analysis.Complex.Basic
-import Mathlib.Analysis.Analytic.Linear
-
-
-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
-  {f₁ f₂ : ℂ → ℂ}
-  {z₀ : ℂ}
-  (hf₁ : AnalyticAt ℂ f₁ z₀)
-  (hf₂ : AnalyticAt ℂ f₂ z₀) :
-  (hf₁.mul 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 AnalyticAt.order_eq_zero_iff
-  {f : ℂ → ℂ}
-  {z₀ : ℂ}
-  (hf : AnalyticAt ℂ f z₀) :
-  hf.order = 0 ↔ f z₀ ≠ 0 := by
-
-  have : (0 : ENat) = (0 : Nat) := by rfl
-  rw [this, AnalyticAt.order_eq_nat_iff hf 0]
-
-  constructor
-  · intro hz
-    obtain ⟨g, _, h₂g, h₃g⟩ := hz
-    simp at h₃g
-    rw [Filter.Eventually.self_of_nhds h₃g]
-    tauto
-  · intro hz
-    use f
-    constructor
-    · exact hf
-    · constructor
-      · exact hz
-      · simp
-
-
-theorem AnalyticAt.order_pow
-  {f : ℂ → ℂ}
-  {z₀ : ℂ}
-  {n : ℕ}
-  (hf : AnalyticAt ℂ f z₀) :
-  (hf.pow n).order = n * hf.order := by
-
-  induction' n with n hn
-  · simp; rw [AnalyticAt.order_eq_zero_iff]; simp
-  · simp
-    simp_rw [add_mul, pow_add]
-    simp
-    rw [AnalyticAt.order_mul (hf.pow n) hf]
-    rw [hn]
-
-
-theorem AnalyticAt.supp_order_toNat
-  {f : ℂ → ℂ}
-  {z₀ : ℂ}
-  (hf : AnalyticAt ℂ f z₀) :
-  hf.order.toNat ≠ 0 → f z₀ = 0 := by
-
-  contrapose
-  intro h₁f
-  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₀ : ℂ}
-  (hf : ∀ᶠ (z : ℂ) in nhds (ℓ z₀), f₁ z = f₂ z)
-  (hℓ : Continuous ℓ) :
-  ∀ᶠ (z : ℂ) in nhds z₀, (f₁ ∘ ℓ) z = (f₂ ∘ ℓ) z := by
-  obtain ⟨t, h₁t, h₂t, h₃t⟩ := eventually_nhds_iff.1 hf
-  apply eventually_nhds_iff.2
-  use ℓ⁻¹' t
-  constructor
-  · intro y hy
-    exact h₁t (ℓ y) hy
-  · constructor
-    · apply IsOpen.preimage
-      exact hℓ
-      exact h₂t
-    · exact h₃t
-
-
-theorem AnalyticAt.order_congr
-  {f₁ f₂ : ℂ → ℂ}
-  {z₀ : ℂ}
-  (hf₁ : AnalyticAt ℂ f₁ z₀)
-  (hf : f₁ =ᶠ[nhds z₀] f₂) :
-  hf₁.order = (hf₁.congr hf).order := by
-
-  by_cases h₁f₁ : hf₁.order = ⊤
-  rw [h₁f₁, eq_comm, AnalyticAt.order_eq_top_iff]
-  rw [AnalyticAt.order_eq_top_iff] at h₁f₁
-  exact Filter.EventuallyEq.rw h₁f₁ (fun x => Eq (f₂ x)) (id (Filter.EventuallyEq.symm hf))
-  --
-  let n := hf₁.order.toNat
-  have hn : hf₁.order = n := Eq.symm (ENat.coe_toNat h₁f₁)
-  rw [hn, eq_comm, AnalyticAt.order_eq_nat_iff]
-  rw [AnalyticAt.order_eq_nat_iff] at hn
-  obtain ⟨g, h₁g, h₂g, h₃g⟩ := hn
-  use g
-  constructor
-  · assumption
-  · constructor
-    · assumption
-    · exact Filter.EventuallyEq.rw h₃g (fun x => Eq (f₂ x)) (id (Filter.EventuallyEq.symm hf))
-
-
-theorem AnalyticAt.order_comp_CLE
-  (ℓ : ℂ ≃L[ℂ] ℂ)
-  {f : ℂ → ℂ}
-  {z₀ : ℂ}
-  (hf : AnalyticAt ℂ f (ℓ z₀)) :
-  hf.order = (hf.comp (ℓ.analyticAt z₀)).order := by
-
-  by_cases h₁f : hf.order = ⊤
-  · rw [h₁f]
-    rw [AnalyticAt.order_eq_top_iff] at h₁f
-    let A := eventually_nhds_comp_composition h₁f ℓ.continuous
-    simp at A
-    rw [AnalyticAt.order_congr (hf.comp (ℓ.analyticAt z₀)) A]
-
-    have : AnalyticAt ℂ (0 : ℂ → ℂ) z₀ := by
-      apply analyticAt_const
-    have : this.order = ⊤ := by
-      rw [AnalyticAt.order_eq_top_iff]
-      simp
-    rw [this]
-  · let n := hf.order.toNat
-    have hn : hf.order = n := Eq.symm (ENat.coe_toNat h₁f)
-    rw [hn]
-    rw [AnalyticAt.order_eq_nat_iff] at hn
-    obtain ⟨g, h₁g, h₂g, h₃g⟩ := hn
-    have A := eventually_nhds_comp_composition h₃g ℓ.continuous
-
-    have t₁ : AnalyticAt ℂ (fun z => ℓ z - ℓ z₀) z₀ := by
-      apply AnalyticAt.sub
-      exact ContinuousLinearEquiv.analyticAt ℓ z₀
-      exact analyticAt_const
-    have t₀ : AnalyticAt ℂ (fun z => (ℓ z - ℓ z₀) ^ n) z₀ := by
-      exact pow t₁ n
-    have : AnalyticAt ℂ (fun z ↦ (ℓ z - ℓ z₀) ^ n • g (ℓ z) : ℂ → ℂ) z₀ := by
-      apply AnalyticAt.mul
-      exact t₀
-      apply AnalyticAt.comp h₁g
-      exact ContinuousLinearEquiv.analyticAt ℓ z₀
-    rw [AnalyticAt.order_congr (hf.comp (ℓ.analyticAt z₀)) A]
-    simp
-
-    rw [AnalyticAt.order_mul t₀ ((h₁g.comp (ℓ.analyticAt z₀)))]
-
-    have : t₁.order = (1 : ℕ) := by
-      rw [AnalyticAt.order_eq_nat_iff]
-      use (fun _ ↦ ℓ 1)
-      simp
-      constructor
-      · exact analyticAt_const
-      · apply Filter.Eventually.of_forall
-        intro x
-        calc ℓ x - ℓ z₀
-        _ = ℓ (x - z₀) := by
-          exact Eq.symm (ContinuousLinearEquiv.map_sub ℓ x z₀)
-        _ = ℓ ((x - z₀) * 1) := by
-          simp
-        _ = (x - z₀) * ℓ 1 := by
-          rw [← smul_eq_mul, ← smul_eq_mul]
-          exact ContinuousLinearEquiv.map_smul ℓ (x - z₀) 1
-
-    have : t₀.order = n := by
-      rw [AnalyticAt.order_pow t₁, this]
-      simp
-
-    rw [this]
-
-    have : (comp h₁g (ContinuousLinearEquiv.analyticAt ℓ z₀)).order = 0 := by
-      rwa [AnalyticAt.order_eq_zero_iff]
-    rw [this]
-
-    simp

Nevanlinna/analyticOn_zeroSet.lean

@@ -1,461 +0,0 @@
-import Mathlib.Analysis.Analytic.Constructions
-import Mathlib.Analysis.Analytic.IsolatedZeros
-import Mathlib.Analysis.Complex.Basic
-import Nevanlinna.analyticAt
-
-
-noncomputable def AnalyticOn.order
-  {f : ℂ → ℂ} {U : Set ℂ} (hf : AnalyticOn ℂ f U) : U → ℕ∞ := fun u ↦ (hf u u.2).order
-
-
-theorem AnalyticOn.order_eq_nat_iff
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  {z₀ : U}
-  (hf : AnalyticOn ℂ f U)
-  (n : ℕ) :
-  hf.order z₀ = ↑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₀ 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 [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 AnalyticOn.support_of_order₁
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  (hf : AnalyticOn ℂ f U) :
-  Function.support hf.order = U.restrict f⁻¹' {0} := by
-  ext u
-  simp [AnalyticOn.order]
-  rw [not_iff_comm, (hf u u.2).order_eq_zero_iff]
-
-
-theorem AnalyticOn.eliminateZeros
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  {A : Finset U}
-  (hf : AnalyticOn ℂ f U)
-  (n : U → ℕ) :
-  (∀ 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 : ℂ → ℂ), 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)
-
-    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₀ (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.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 : AnalyticOn ℂ 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 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.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, AnalyticOn.order]
-    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]
-
-  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 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 = (∏ 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, AnalyticOn.order]
-    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
-
-  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 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 = (∏ᶠ 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, AnalyticOn.order]
-    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
-
-  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/bilinear.lean

@@ -32,13 +32,24 @@ orthonormal basis `v` as `∑ i, (v i) ⊗ₜ[ℝ] (v i)`.
 open TensorProduct
 
 
+lemma OrthonormalBasis.sum_repr'
+  {𝕜 : Type*} [RCLike 𝕜]
+  {E : Type*} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
+  [Fintype ι]
+  (b : OrthonormalBasis ι 𝕜 E)
+  (v : E) :
+  v = ∑ i, ⟪b i, v⟫_𝕜 • (b i) := by
+  nth_rw 1 [← (b.sum_repr v)]
+  simp_rw [b.repr_apply_apply v]
+
+
 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 : Type*) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] 
   : E ⊗[ℝ] E := ∑ i, ((stdOrthonormalBasis ℝ E) i) ⊗ₜ[ℝ] ((stdOrthonormalBasis ℝ E) i)
 
 
@@ -53,9 +64,9 @@ theorem InnerProductSpace.canonicalCovariantTensorRepresentation
     right
     arg 2
     intro i
-    rw [← w.sum_repr' (v 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]

Nevanlinna/cauchyRiemann.lean

@@ -45,8 +45,8 @@ theorem CauchyRiemann₃ : (DifferentiableAt ℂ f z)
 
 
 theorem CauchyRiemann₄
-  {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F]
-  {f : ℂ → F} :
+  {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] 
+  {f : ℂ → F} : 
   (Differentiable ℂ f) → partialDeriv ℝ Complex.I f = Complex.I • partialDeriv ℝ 1 f := by
   intro h
   unfold partialDeriv
@@ -58,13 +58,13 @@ theorem CauchyRiemann₄
     simp
     rw [← mul_one Complex.I]
     rw [← smul_eq_mul]
+    rw [ContinuousLinearMap.map_smul_of_tower (fderiv ℂ f w) Complex.I 1]
   conv =>
     right
     right
     intro w
     rw [DifferentiableAt.fderiv_restrictScalars ℝ (h w)]
-  funext w
-  simp
+
 
 theorem CauchyRiemann₅ {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] {f : ℂ → F} {z : ℂ} : (DifferentiableAt ℂ f z)
   → partialDeriv ℝ Complex.I f z = Complex.I • partialDeriv ℝ 1 f z := by
@@ -77,8 +77,8 @@ theorem CauchyRiemann₅ {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F]
     simp
     rw [← mul_one Complex.I]
     rw [← smul_eq_mul]
+    rw [ContinuousLinearMap.map_smul_of_tower (fderiv ℂ f z) Complex.I 1]
   conv =>
     right
     right
     rw [DifferentiableAt.fderiv_restrictScalars ℝ h]
-  simp

Nevanlinna/complexHarmonic.lean

@@ -1,9 +1,9 @@
 import Nevanlinna.laplace
 
 variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
-variable {F₁ : Type*} [NormedAddCommGroup F₁] [NormedSpace ℂ F₁]
+variable {F₁ : Type*} [NormedAddCommGroup F₁] [NormedSpace ℂ F₁] [CompleteSpace F₁]
 variable {G : Type*} [NormedAddCommGroup G] [NormedSpace ℝ G]
-variable {G₁ : Type*} [NormedAddCommGroup G₁] [NormedSpace ℂ G₁]
+variable {G₁ : Type*} [NormedAddCommGroup G₁] [NormedSpace ℂ G₁] [CompleteSpace G₁]
 
 
 def Harmonic (f : ℂ → F) : Prop :=
@@ -33,7 +33,7 @@ theorem HarmonicAt_iff
     · constructor
       · exact Set.mem_inter h₂s₁ h₃s₂
       · constructor
-        · exact h₃s₁.mono Set.inter_subset_left
+        · exact h₃s₁.mono (Set.inter_subset_left s₁ s₂)
         · intro z hz
           exact h₂t₂ (h₁s₂ hz.2)
   · intro hyp
@@ -47,24 +47,6 @@ theorem HarmonicAt_iff
       · apply (IsOpen.mem_nhds_iff h₁s).2 h₂s
       · exact h₂f
 
-theorem HarmonicAt_isOpen
-  (f : ℂ → F) :
-  IsOpen { x : ℂ | HarmonicAt f x } := by
-
-  rw [← subset_interior_iff_isOpen]
-  intro x hx
-  simp at hx
-  obtain ⟨s, h₁s, h₂s, h₃s⟩ := HarmonicAt_iff.1 hx
-  use s
-  constructor
-  · simp
-    constructor
-    · exact h₁s
-    · intro x hx
-      simp
-      rw [HarmonicAt_iff]
-      use s
-  · exact h₂s
 
 theorem HarmonicAt_eventuallyEq {f₁ f₂ : ℂ → F} {x : ℂ} (h : f₁ =ᶠ[nhds x] f₂) : HarmonicAt f₁ x ↔ HarmonicAt f₂ x := by
   constructor

Nevanlinna/divisor.lean

@@ -1,139 +0,0 @@
-import Nevanlinna.analyticAt
-
-
-structure Divisor where
-  toFun : ℂ → ℤ
-  discreteSupport : DiscreteTopology (Function.support toFun)
-
-instance : CoeFun Divisor (fun _ ↦ ℂ → ℤ) where
-coe := Divisor.toFun
-attribute [coe] Divisor.toFun
-
-
-
-noncomputable def Divisor.deg
-  (D : Divisor) : ℤ := ∑ᶠ z, D z
-
-noncomputable def Divisor.n_trunk
-  (D : Divisor) : ℤ → ℝ → ℤ := fun k r ↦ ∑ᶠ z ∈ Metric.ball 0 r, min k (D z)
-
-noncomputable def Divisor.n
-  (D : Divisor) : ℝ → ℤ := fun r ↦ ∑ᶠ z ∈ Metric.ball 0 r, D z
-
-noncomputable def Divisor.N_trunk
-  (D : Divisor) : ℤ → ℝ → ℝ := fun k r ↦ ∫ (t : ℝ) in (1)..r, (D.n_trunk k t) / t
-
-theorem Divisor.compactSupport
-  (D : Divisor)
-  {U : Set ℂ}
-  (h₁U : IsCompact U)
-  (h₂U : Function.support D ⊆ U) :
-  Set.Finite (Function.support D) := by
-  sorry
-
-
-noncomputable def AnalyticOn.zeroDivisor
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  (hf : AnalyticOn ℂ f U) :
-  Divisor where
-
-    toFun := by
-      intro z
-      if hz : z ∈ U then
-        exact ((hf z hz).order.toNat : ℤ)
-      else
-        exact 0
-
-    discreteSupport := by
-      simp_rw [← singletons_open_iff_discrete]
-      simp_rw [Metric.isOpen_singleton_iff]
-      simp
-
-      --  simp only [dite_eq_ite, gt_iff_lt, Subtype.forall, Function.mem_support, ne_eq, ite_eq_else, Classical.not_imp, not_or, Subtype.mk.injEq]
-
-      intro a ha ⟨h₁a, h₂a⟩
-      obtain ⟨g, h₁g, h₂g, h₃g⟩ := (AnalyticAt.order_neq_top_iff (hf a ha)).1 h₂a
-      rw [Metric.eventually_nhds_iff_ball] at h₃g
-
-      have : ∃ ε > 0, ∀ y ∈ Metric.ball (↑a) ε, g y ≠ 0 := by
-        have h₄g : ContinuousAt g a :=
-          AnalyticAt.continuousAt h₁g
-        have : {0}ᶜ ∈ nhds (g a) := 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 hy ⟨h₁y, h₂y⟩ h₃
-
-      have h'₂y : ↑y ∈ Metric.ball (↑a) ε₂ := by
-        simp
-        calc dist y a
-        _ < min ε₁ ε₂ := by assumption
-        _ ≤ ε₂ := by exact min_le_right ε₁ ε₂
-
-      have h₃y : ↑y ∈ Metric.ball (↑a) ε₁ := by
-        simp
-        calc dist y a
-        _ < min ε₁ ε₂ := by assumption
-        _ ≤ ε₁ := by exact min_le_left ε₁ ε₂
-
-      have F := h₂ε₂ y h'₂y
-      have : f y = 0 := by
-        rw [AnalyticAt.order_eq_zero_iff (hf y hy)] at h₁y
-        tauto
-      rw [this] at F
-      simp at F
-
-      have : g y ≠ 0 := by
-        exact h₁ε₁.2 y h₃y
-      simp [this] at F
-      rw [sub_eq_zero] at F
-      tauto
-
-
-theorem AnalyticOn.support_of_zeroDivisor
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  (hf : AnalyticOn ℂ f U) :
-  Function.support hf.zeroDivisor ⊆ U := by
-
-  intro z
-  contrapose
-  intro hz
-  dsimp [AnalyticOn.zeroDivisor]
-  simp
-  tauto
-
-
-theorem AnalyticOn.support_of_zeroDivisor₂
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  (hf : AnalyticOn ℂ f U) :
-  Function.support hf.zeroDivisor ⊆ f⁻¹' {0} := by
-
-  intro z hz
-  dsimp [AnalyticOn.zeroDivisor] at hz
-  have t₀ := hf.support_of_zeroDivisor hz
-  simp [hf.support_of_zeroDivisor hz] at hz
-  let A := hz.1
-  let C := (hf z t₀).order_eq_zero_iff
-  simp
-  rw [C] at A
-  tauto

Nevanlinna/firstMain.lean

@@ -1,21 +0,0 @@
-import Mathlib.Analysis.Analytic.Meromorphic
-import Nevanlinna.holomorphic_JensenFormula
-
-open Real
-
-variable (f : ℂ → ℂ)
-variable {h₁f : MeromorphicOn f ⊤}
-variable {h₂f : f 0 ≠ 0}
-
-
-
-noncomputable def Nevanlinna.n : ℝ → ℤ := 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
-
-noncomputable def integratedCounting : ℝ → ℝ := by
-  intro r
-  -- Issue here: for s on the boundary of the ball, zero comes out.
-  exact ∑ᶠ s, (h₁f.order s).toNat * log (r * ‖s.1‖⁻¹)

Nevanlinna/harmonicAt.examples.lean

@@ -1,5 +1,5 @@
 import Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
-import Nevanlinna.harmonicAt
+import Nevanlinna.complexHarmonic
 import Nevanlinna.holomorphicAt
 
 variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F]

Nevanlinna/harmonicAt_meanValue.lean

@@ -1,131 +0,0 @@
-import Mathlib.Analysis.NormedSpace.Pointwise
-import Mathlib.Topology.MetricSpace.Thickening
-import Mathlib.Analysis.Complex.CauchyIntegral
-import Nevanlinna.holomorphic_examples
-
-theorem harmonic_meanValue
-  {f : ℂ → ℝ}
-  {z : ℂ}
-  (ρ R : ℝ)
-  (hR : 0 < R)
-  (hρ : R < ρ)
-  (hf : ∀ x ∈ Metric.ball z ρ , HarmonicAt f x) :
-  (∫ (x : ℝ) in (0)..2 * Real.pi, f (circleMap z R x)) = 2 * Real.pi * f z
-  := by
-
-  obtain ⟨F, h₁F, h₂F⟩ := harmonic_is_realOfHolomorphic (gt_trans hρ hR) hf
-
-  have hrρ : Metric.ball z R ⊆ Metric.ball z ρ := by
-    intro x hx
-    exact gt_trans hρ hx
-
-  have reg₀F : DifferentiableOn ℂ F (Metric.ball z ρ) := by
-    intro x hx
-    apply DifferentiableAt.differentiableWithinAt
-    apply HolomorphicAt.differentiableAt (h₁F x _)
-    exact hx
-
-  have reg₁F : DifferentiableOn ℂ F (Metric.ball z R) := by
-    intro x hx
-    apply DifferentiableAt.differentiableWithinAt
-    apply HolomorphicAt.differentiableAt (h₁F x _)
-    exact hrρ hx
-
-  have : (∮ (x : ℂ) in C(z, R), (x - z)⁻¹ • F x) = (2 * ↑Real.pi * Complex.I) • F z := by
-    let s : Set ℂ := ∅
-    let hs : s.Countable := Set.countable_empty
-    let _ : ℂ := 0
-    have hw : (z : ℂ) ∈ Metric.ball z R := Metric.mem_ball_self hR
-    have hc : ContinuousOn F (Metric.closedBall z R) := by
-      apply reg₀F.continuousOn.mono
-      intro x hx
-      simp at hx
-      simp
-      linarith
-    have hd : ∀ x ∈ Metric.ball z R \ s, DifferentiableAt ℂ F x := by
-      intro x hx
-      let A := reg₁F x hx.1
-      apply A.differentiableAt
-      apply (IsOpen.mem_nhds_iff ?hs).mpr
-      exact hx.1
-      exact Metric.isOpen_ball
-    let CIF := Complex.circleIntegral_sub_inv_smul_of_differentiable_on_off_countable hs hw hc hd
-    simp at CIF
-    assumption
-
-  unfold circleIntegral at this
-  simp_rw [deriv_circleMap] at this
-
-  have t₁ {θ : ℝ} : (circleMap 0 R θ * Complex.I) • (circleMap 0 R θ)⁻¹ • F (circleMap z R θ) = Complex.I • F (circleMap z R θ) := by
-    rw [← smul_assoc]
-    congr 1
-    simp
-    nth_rw 1 [mul_comm]
-    rw [← mul_assoc]
-    simp
-    apply inv_mul_cancel₀
-    apply circleMap_ne_center
-    exact Ne.symm (ne_of_lt hR)
-  have t'₁  {θ : ℝ} : circleMap 0 R θ = circleMap z R θ - z := by
-    exact Eq.symm (circleMap_sub_center z R θ)
-  simp_rw [← t'₁, t₁] at this
-  simp at this
-
-  have t₂ : Complex.reCLM (-Complex.I * (Complex.I * ∫ (x : ℝ) in (0)..2 * Real.pi, F (circleMap z R x))) = Complex.reCLM (-Complex.I * (2 * ↑Real.pi * Complex.I * F z)) := by
-    rw [this]
-  simp at t₂
-  have xx {x : ℝ} : (F (circleMap z R x)).re = f (circleMap z R x) := by
-    rw [← h₂F]
-    simp
-    simp
-    rw [Complex.dist_eq]
-    rw [circleMap_sub_center]
-    simp
-    rwa [abs_of_nonneg (le_of_lt hR)]
-  have x₁ {z : ℂ} : z.re = Complex.reCLM z := by rfl
-  rw [x₁] at t₂
-  rw [← ContinuousLinearMap.intervalIntegral_comp_comm] at t₂
-  simp at t₂
-  simp_rw [xx] at t₂
-  have x₁ {z : ℂ} : z.re = Complex.reCLM z := by rfl
-  rw [x₁] at t₂
-  have : Complex.reCLM (F z) = f z := by
-    apply h₂F
-    simp
-    exact gt_trans hρ hR
-  rw [this] at t₂
-  exact t₂
-
-  -- IntervalIntegrable (fun x => F (circleMap 0 1 x)) MeasureTheory.volume 0 (2 * Real.pi)
-  apply ContinuousOn.intervalIntegrable
-  apply ContinuousOn.comp reg₀F.continuousOn _
-  intro θ _
-  simp
-  rw [Complex.dist_eq, circleMap_sub_center]
-  simp
-  rwa [abs_of_nonneg (le_of_lt hR)]
-  apply Continuous.continuousOn
-  exact continuous_circleMap z R
-
-/- Probably not optimal yet. We want a statements that requires harmonicity in
-the interior and continuity on the closed ball.
--/
-
-
-theorem harmonic_meanValue₁
-  {f : ℂ → ℝ}
-  {z : ℂ}
-  (R : ℝ)
-  (hR : 0 < R)
-  (hf : ∀ x ∈ Metric.closedBall z R , HarmonicAt f x) :
-  (∫ (x : ℝ) in (0)..2 * Real.pi, f (circleMap z R x)) = 2 * Real.pi * f z := by
-
-  obtain ⟨e, h₁e, h₂e⟩ := IsCompact.exists_thickening_subset_open (isCompact_closedBall z R) (HarmonicAt_isOpen f) hf
-  rw [thickening_closedBall] at h₂e
-  apply harmonic_meanValue (e + R) R
-  assumption
-  norm_num
-  assumption
-  exact fun x a => h₂e a
-  assumption
-  linarith

Nevanlinna/holomorphic.lean

@@ -2,8 +2,8 @@ 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]
+variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F]
+variable {G : Type*} [NormedAddCommGroup G] [NormedSpace ℂ G] [CompleteSpace G]
 
 def HolomorphicAt (f : E → F) (x : E) : Prop :=
   ∃ s ∈ nhds x, ∀ z ∈ s, DifferentiableAt ℂ f z
@@ -33,21 +33,6 @@ theorem HolomorphicAt_iff
     · 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} :
@@ -120,7 +105,6 @@ theorem HolomorphicAt_neg
 
 
 theorem HolomorphicAt_contDiffAt
-  [CompleteSpace F]
   {f : ℂ → F}
   {z : ℂ}
   (hf : HolomorphicAt f z) :
@@ -153,11 +137,12 @@ theorem CauchyRiemann'₅
     simp
     rw [← mul_one Complex.I]
     rw [← smul_eq_mul]
+    rw [ContinuousLinearMap.map_smul_of_tower (fderiv ℂ f z) Complex.I 1]
   conv =>
     right
     right
     rw [DifferentiableAt.fderiv_restrictScalars ℝ h]
-  simp
+
 
 theorem CauchyRiemann'₆
   {f : ℂ → F}

Nevanlinna/holomorphic.primitive.lean

@@ -3,10 +3,8 @@ import Mathlib.Analysis.SpecialFunctions.Integrals
 import Mathlib.MeasureTheory.Integral.DivergenceTheorem
 import Mathlib.MeasureTheory.Integral.IntervalIntegral
 import Mathlib.MeasureTheory.Function.LocallyIntegrable
-import Nevanlinna.partialDeriv
-import Nevanlinna.cauchyRiemann
 
-/-
+
 noncomputable def partialDeriv
   {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
   {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] : E → (E → F) → (E → F) :=
@@ -27,7 +25,6 @@ theorem partialDeriv_compContLinAt
   rw [fderiv.comp x (ContinuousLinearMap.differentiableAt l) h]
   simp
 
-
 theorem partialDeriv_compCLE
   {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
   {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F]
@@ -88,7 +85,7 @@ theorem partialDeriv_smul'₂
 theorem CauchyRiemann₄
   {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] 
   {f : ℂ → F} : 
-  (Differentiable ℂ f) → partialDeriv ℝ Complex.I f = Complex.I • partialDeriv ℝ 1 f := by
+  (Differentiable ℂ f) → partialDeriv Complex.I f = Complex.I • partialDeriv 1 f := by
   intro h
   unfold partialDeriv
 
@@ -99,14 +96,12 @@ theorem CauchyRiemann₄
     simp
     rw [← mul_one Complex.I]
     rw [← smul_eq_mul]
+    rw [ContinuousLinearMap.map_smul_of_tower (fderiv ℂ f w) Complex.I 1]
   conv =>
     right
     right
     intro w
     rw [DifferentiableAt.fderiv_restrictScalars ℝ (h w)]
-  funext w
-  simp
--/
 
 
 theorem MeasureTheory.integral2_divergence₃
@@ -205,12 +200,12 @@ theorem integral_divergence₅
     rw [this]
     apply ContDiff.comp
     exact contDiff_const_smul _
-    exact h₁f  
+    exact h₁f
 
   let A := integral_divergence₄ (-Complex.I • F) F h₁g h₁f lowerLeft.re upperRight.im upperRight.re lowerLeft.im
-  have {z : ℂ} : fderiv ℝ F z Complex.I = partialDeriv ℝ Complex.I F z := by rfl
+  have {z : ℂ} : fderiv ℝ F z Complex.I = partialDeriv _ F z := by rfl
   conv at A in (fderiv ℝ F _) _ => rw [this]
-  have {z : ℂ} : fderiv ℝ (-Complex.I • F) z 1 = partialDeriv ℝ 1 (-Complex.I • F) z := by rfl
+  have {z : ℂ} : fderiv ℝ (-Complex.I • F) z 1 = partialDeriv _ (-Complex.I • F) z := by rfl
   conv at A in (fderiv ℝ (-Complex.I • F) _) _ => rw [this]
   conv at A =>
     left
@@ -296,17 +291,26 @@ theorem primitive_fderivAtBasepointZero
     fun_prop
   have t₂ {a b : ℝ} : IntervalIntegrable (fun x_1 => f { re := a, im := x_1 }) MeasureTheory.volume 0 b := by
     apply Continuous.intervalIntegrable
-    apply Continuous.comp hf
-    have : (Complex.mk a) = (fun x => Complex.I • Complex.ofRealCLM x + { re := a, im := 0 }) := by
+    apply Continuous.comp
+    exact hf
+    have : ((fun x => { re := a, im := x }) : ℝ → ℂ) = (fun x => { re := a, im := 0 } + { re := 0, im := x }) := by
       funext x
       apply Complex.ext
       rw [Complex.add_re]
       simp
+      rw [Complex.add_im]
       simp
     rw [this]
     apply Continuous.add
-    continuity
     fun_prop
+    have : (fun x => { re := 0, im := x } : ℝ → ℂ) = Complex.I • Complex.ofRealCLM := by
+      funext x
+      simp
+      have : (x : ℂ) = {re := x, im := 0} := by rfl
+      rw [this]
+      rw [Complex.I_mul]
+      simp
+    continuity
 
   have t₃ {a : ℝ} : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 a := by
     apply Continuous.intervalIntegrable
@@ -485,11 +489,11 @@ theorem primitive_translation
   simp
 
 
-theorem primitive_hasDerivAtBasepoint
+theorem primitive_fderivAtBasepoint
   {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
-  {f : ℂ  → E}
-  (hf : Continuous f)   
-  (z₀ : ℂ) :
+  {z₀ : ℂ}
+  (f : ℂ  → E)
+  (hf : Continuous f) :
   HasDerivAt (primitive z₀ f) (f z₀) z₀ := by
 
   let g := f ∘ fun z ↦ z + z₀
@@ -553,7 +557,7 @@ lemma integrability₂
   apply Continuous.intervalIntegrable
   apply Continuous.comp
   exact Differentiable.continuous hf
-  have : (Complex.mk b) = (fun x => Complex.I • Complex.ofRealCLM x + { re := b, im := 0 }) := by
+  have : ((fun x => { re := b, im := x }) : ℝ → ℂ) = (fun x => Complex.I • Complex.ofRealCLM x + { re := b, im := 0 }) := by
     funext x
     apply Complex.ext
     rw [Complex.add_re]
@@ -597,70 +601,15 @@ theorem primitive_additivity
   abel
 
 
-theorem primitive_hasDerivAt
+theorem primitive_fderiv
   {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
-  {f : ℂ  → E}
-  (hf : Differentiable ℂ f)
-  (z₀ z : ℂ) :
+  {z₀ z : ℂ}
+  (f : ℂ  → E)
+  (hf : Differentiable ℂ f) :
   HasDerivAt (primitive z₀ f) (f z) z := by
   rw [primitive_additivity f hf z₀ z]
   rw [← add_zero (f z)]
   apply HasDerivAt.add
-  apply primitive_hasDerivAtBasepoint
+  apply primitive_fderivAtBasepoint
   exact hf.continuous
   apply hasDerivAt_const
-
-
-theorem primitive_differentiable
-  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
-  {f : ℂ  → E}
-  (hf : Differentiable ℂ f)
-  (z₀ : ℂ) :
-  Differentiable ℂ (primitive z₀ f) := by
-  intro z
-  exact (primitive_hasDerivAt hf z₀ z).differentiableAt 
-
-
-theorem primitive_hasFderivAt
-  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
-  {f : ℂ  → E}
-  (hf : Differentiable ℂ f)
-  (z₀ : ℂ) :
-  ∀ z, HasFDerivAt (primitive z₀ f) ((ContinuousLinearMap.lsmul ℂ ℂ).flip (f z)) z := by
-  intro z
-  rw [hasFDerivAt_iff_hasDerivAt]
-  simp    
-  exact primitive_hasDerivAt hf z₀ z
-
-
-theorem primitive_hasFderivAt'
-  {f : ℂ  → ℂ}
-  (hf : Differentiable ℂ f)
-  (z₀ : ℂ) :
-  ∀ z, HasFDerivAt (primitive z₀ f) (ContinuousLinearMap.lsmul ℂ ℂ (f z)) z := by
-  intro z
-  rw [hasFDerivAt_iff_hasDerivAt]
-  simp    
-  exact primitive_hasDerivAt hf z₀ z
-
-
-theorem primitive_fderiv
-  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
-  {f : ℂ  → E}
-  (hf : Differentiable ℂ f)
-  (z₀ : ℂ) :
-  ∀ z, (fderiv ℂ (primitive z₀ f) z) = (ContinuousLinearMap.lsmul ℂ ℂ).flip (f z) := by
-  intro z
-  apply HasFDerivAt.fderiv
-  exact primitive_hasFderivAt hf z₀ z
-
-
-theorem primitive_fderiv'
-  {f : ℂ  → ℂ}
-  (hf : Differentiable ℂ f)
-  (z₀ : ℂ) :
-  ∀ z, (fderiv ℂ (primitive z₀ f) z) = ContinuousLinearMap.lsmul ℂ ℂ (f z) := by
-  intro z
-  apply HasFDerivAt.fderiv
-  exact primitive_hasFderivAt' hf z₀ z
-

Nevanlinna/holomorphicAt.lean

@@ -1,4 +1,4 @@
-import Mathlib.Analysis.Complex.CauchyIntegral
+import Mathlib.Analysis.Complex.TaylorSeries
 import Nevanlinna.cauchyRiemann
 
 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
@@ -33,21 +33,6 @@ theorem HolomorphicAt_iff
     · assumption
 
 
-theorem Differentiable.holomorphicAt
-  {f : E → F}
-  (hf : Differentiable ℂ f)
-  {x : E} :
-  HolomorphicAt f x := by
-  apply HolomorphicAt_iff.2
-  use Set.univ
-  constructor
-  · exact isOpen_univ
-  · constructor
-    · exact trivial
-    · intro z _
-      exact hf z
-
-
 theorem HolomorphicAt_isOpen
   (f : E → F) :
   IsOpen { x : E | HolomorphicAt f x } := by
@@ -110,38 +95,6 @@ theorem HolomorphicAt_neg
     exact h₂UF z hz
 
 
-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 AnalyticAt.holomorphicAt
-  [CompleteSpace F]
-  {f : ℂ → F}
-  {x : ℂ} :
-  AnalyticAt ℂ f x → HolomorphicAt f x := by
-  intro hf
-  rw [HolomorphicAt_iff]
-  use {x : ℂ | AnalyticAt ℂ f x}
-  constructor
-  · exact isOpen_analyticAt ℂ f
-  · constructor
-    · simpa
-    · intro z hz
-      simp at hz
-      exact differentiableAt hz
-
-
 theorem HolomorphicAt.contDiffAt
   [CompleteSpace F]
   {f : ℂ → F}

Nevanlinna/holomorphic_JensenFormula.lean

@@ -1,449 +0,0 @@
-import Mathlib.Analysis.Complex.CauchyIntegral
-import Mathlib.Analysis.Analytic.IsolatedZeros
-import Nevanlinna.analyticOn_zeroSet
-import Nevanlinna.harmonicAt_examples
-import Nevanlinna.harmonicAt_meanValue
-import Nevanlinna.specialFunctions_CircleIntegral_affine
-
-open Real
-
-
-
-theorem jensen_case_R_eq_one
-  (f : ℂ → ℂ)
-  (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
-
-  have h₁U : IsPreconnected (Metric.closedBall (0 : ℂ) 1) :=
-    (convex_closedBall (0 : ℂ) 1).isPreconnected
-
-  have h₂U : IsCompact (Metric.closedBall (0 : ℂ) 1) :=
-    isCompact_closedBall 0 1
-
-  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⟩ := 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
-    apply AnalyticAt.holomorphicAt
-    exact h₁F z h₁z
-
-  let G := fun z ↦ log ‖F z‖ + ∑ s ∈ (finiteZeros h₁U h₂U h₁f h'₂f).toFinset, (h₁f.order s).toNat * log ‖z - s‖
-
-  have decompose_f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, f z ≠ 0 → log ‖f z‖ = G z := by
-    intro z h₁z h₂z
-
-    conv =>
-      left
-      arg 1
-      rw [h₃F]
-      rw [smul_eq_mul]
-      rw [norm_mul]
-      rw [norm_prod]
-      left
-      arg 2
-      intro b
-      rw [norm_pow]
-    simp only [Complex.norm_eq_abs, Finset.univ_eq_attach]
-    rw [Real.log_mul]
-    rw [Real.log_prod]
-    conv =>
-      left
-      left
-      arg 2
-      intro s
-      rw [Real.log_pow]
-    dsimp [G]
-    abel
-
-    -- ∀ x ∈ ⋯.toFinset, Complex.abs (z - ↑x) ^ (h'₁f.order x).toNat ≠ 0
-    have : ∀ x ∈ (finiteZeros h₁U h₂U h₁f h'₂f).toFinset, Complex.abs (z - ↑x) ^ (h₁f.order x).toNat ≠ 0 := by
-      intro s hs
-      simp at hs
-      simp
-      intro h₂s
-      rw [h₂s] at h₂z
-      tauto
-    exact this
-
-    -- ∏ x ∈ ⋯.toFinset, Complex.abs (z - ↑x) ^ (h'₁f.order x).toNat ≠ 0
-    have : ∀ x ∈ (finiteZeros h₁U h₂U h₁f h'₂f).toFinset, Complex.abs (z - ↑x) ^ (h₁f.order x).toNat ≠ 0 := by
-      intro s hs
-      simp at hs
-      simp
-      intro h₂s
-      rw [h₂s] at h₂z
-      tauto
-    rw [Finset.prod_ne_zero_iff]
-    exact this
-
-    -- Complex.abs (F z) ≠ 0
-    simp
-    exact h₂F z h₁z
-
-
-  have int_logAbs_f_eq_int_G : ∫ (x : ℝ) in (0)..2 * π, log ‖f (circleMap 0 1 x)‖ = ∫ (x : ℝ) in (0)..2 * π, G (circleMap 0 1 x) := by
-
-    rw [intervalIntegral.integral_congr_ae]
-    rw [MeasureTheory.ae_iff]
-    apply Set.Countable.measure_zero
-    simp
-
-    have t₀ : {a | a ∈ Ι 0 (2 * π) ∧ ¬log ‖f (circleMap 0 1 a)‖ = G (circleMap 0 1 a)}
-      ⊆ (circleMap 0 1)⁻¹' (Metric.closedBall 0 1 ∩ f⁻¹' {0}) := by
-      intro a ha
-      simp at ha
-      simp
-      by_contra C
-      have : (circleMap 0 1 a) ∈ Metric.closedBall 0 1 :=
-        circleMap_mem_closedBall 0 (zero_le_one' ℝ) a
-      exact ha.2 (decompose_f (circleMap 0 1 a) this C)
-
-    apply Set.Countable.mono t₀
-    apply Set.Countable.preimage_circleMap
-    apply Set.Finite.countable
-    let A := finiteZeros h₁U h₂U h₁f h'₂f
-
-    have : (Metric.closedBall 0 1 ∩ f ⁻¹' {0}) = (Metric.closedBall 0 1).restrict f ⁻¹' {0} := by
-      ext z
-      simp
-      tauto
-    rw [this]
-    exact Set.Finite.image Subtype.val A
-    exact Ne.symm (zero_ne_one' ℝ)
-
-
-  have decompose_int_G : ∫ (x : ℝ) in (0)..2 * π, G (circleMap 0 1 x)
-    = (∫ (x : ℝ) in (0)..2 * π, log (Complex.abs (F (circleMap 0 1 x))))
-        + ∑ x ∈ (finiteZeros h₁U h₂U h₁f h'₂f).toFinset, (h₁f.order x).toNat * ∫ (x_1 : ℝ) in (0)..2 * π, log (Complex.abs (circleMap 0 1 x_1 - ↑x)) := by
-    dsimp [G]
-    rw [intervalIntegral.integral_add]
-    rw [intervalIntegral.integral_finset_sum]
-    simp_rw [intervalIntegral.integral_const_mul]
-
-    --  ∀ i ∈ (finiteZeros h₁U h₂U h'₁f h'₂f).toFinset,
-    --  IntervalIntegrable (fun x => (h'₁f.order i).toNat *
-    --    log (Complex.abs (circleMap 0 1 x - ↑i))) MeasureTheory.volume 0 (2 * π)
-    intro i _
-    apply IntervalIntegrable.const_mul
-    --simp at this
-    by_cases h₂i : ‖i.1‖ = 1
-    -- case pos
-    exact int'₂ h₂i
-    -- case neg
-    apply Continuous.intervalIntegrable
-    apply continuous_iff_continuousAt.2
-    intro x
-    have : (fun x => log (Complex.abs (circleMap 0 1 x - ↑i))) = log ∘ Complex.abs ∘ (fun x ↦ circleMap 0 1 x - ↑i) :=
-      rfl
-    rw [this]
-    apply ContinuousAt.comp
-    apply Real.continuousAt_log
-    simp
-
-    by_contra ha'
-    conv at h₂i =>
-      arg 1
-      rw [← ha']
-      rw [Complex.norm_eq_abs]
-      rw [abs_circleMap_zero 1 x]
-      simp
-    tauto
-    apply ContinuousAt.comp
-    apply Complex.continuous_abs.continuousAt
-    fun_prop
-    -- IntervalIntegrable (fun x => log (Complex.abs (F (circleMap 0 1 x)))) MeasureTheory.volume 0 (2 * π)
-    apply Continuous.intervalIntegrable
-    apply continuous_iff_continuousAt.2
-    intro x
-    have : (fun x => log (Complex.abs (F (circleMap 0 1 x)))) = log ∘ Complex.abs ∘ F ∘ (fun x ↦ circleMap 0 1 x) :=
-      rfl
-    rw [this]
-    apply ContinuousAt.comp
-    apply Real.continuousAt_log
-    simp [h₂F]
-    -- ContinuousAt (⇑Complex.abs ∘ F ∘ fun x => circleMap 0 1 x) x
-    apply ContinuousAt.comp
-    apply Complex.continuous_abs.continuousAt
-    apply ContinuousAt.comp
-    apply DifferentiableAt.continuousAt (𝕜 := ℂ )
-    apply HolomorphicAt.differentiableAt
-    simp [h'₁F]
-    -- ContinuousAt (fun x => circleMap 0 1 x) x
-    apply Continuous.continuousAt
-    apply continuous_circleMap
-
-    have : (fun x => ∑ s ∈ (finiteZeros h₁U h₂U h₁f h'₂f).toFinset, (h₁f.order s).toNat * log (Complex.abs (circleMap 0 1 x - ↑s)))
-      = ∑ s ∈ (finiteZeros h₁U h₂U h₁f h'₂f).toFinset, (fun x => (h₁f.order s).toNat * log (Complex.abs (circleMap 0 1 x - ↑s))) := by
-      funext x
-      simp
-    rw [this]
-    apply IntervalIntegrable.sum
-    intro i _
-    apply IntervalIntegrable.const_mul
-    --have : i.1 ∈ Metric.closedBall (0 : ℂ) 1 := i.2
-    --simp at this
-    by_cases h₂i : ‖i.1‖ = 1
-    -- case pos
-    exact int'₂ h₂i
-    -- case neg
-    --have : i.1 ∈ Metric.ball (0 : ℂ) 1 := by sorry
-    apply Continuous.intervalIntegrable
-    apply continuous_iff_continuousAt.2
-    intro x
-    have : (fun x => log (Complex.abs (circleMap 0 1 x - ↑i))) = log ∘ Complex.abs ∘ (fun x ↦ circleMap 0 1 x - ↑i) :=
-      rfl
-    rw [this]
-    apply ContinuousAt.comp
-    apply Real.continuousAt_log
-    simp
-
-    by_contra ha'
-    conv at h₂i =>
-      arg 1
-      rw [← ha']
-      rw [Complex.norm_eq_abs]
-      rw [abs_circleMap_zero 1 x]
-      simp
-    tauto
-    apply ContinuousAt.comp
-    apply Complex.continuous_abs.continuousAt
-    fun_prop
-
-  have t₁ : (∫ (x : ℝ) in (0)..2 * Real.pi, log ‖F (circleMap 0 1 x)‖) = 2 * Real.pi * log ‖F 0‖ := by
-    let logAbsF := fun w ↦ Real.log ‖F w‖
-    have t₀ : ∀ z ∈ Metric.closedBall 0 1, HarmonicAt logAbsF z := by
-      intro z hz
-      apply logabs_of_holomorphicAt_is_harmonic
-      apply h'₁F z hz
-      exact h₂F z hz
-
-    apply harmonic_meanValue₁ 1 Real.zero_lt_one t₀
-
-  simp_rw [← Complex.norm_eq_abs] at decompose_int_G
-  rw [t₁] at decompose_int_G
-
-  conv at decompose_int_G =>
-    right
-    right
-    arg 2
-    intro x
-    right
-    rw [int₃ x.2]
-  simp at decompose_int_G
-
-  rw [int_logAbs_f_eq_int_G]
-  rw [decompose_int_G]
-  rw [h₃F]
-  simp
-  have {l : ℝ} : π⁻¹ * 2⁻¹ * (2 * π * l) = l := by
-    calc π⁻¹ * 2⁻¹ * (2 * π * l)
-    _ = π⁻¹ * (2⁻¹ * 2) * π * l := by ring
-    _ = π⁻¹ * π * l := by ring
-    _ = (π⁻¹ * π) * l := by ring
-    _ = 1 * l := by
-      rw [inv_mul_cancel₀]
-      exact pi_ne_zero
-    _ = l := by simp
-  rw [this]
-  rw [log_mul]
-  rw [log_prod]
-  simp
-
-  rw [finsum_eq_sum_of_support_subset _ (s := (finiteZeros h₁U h₂U h₁f h'₂f).toFinset)]
-  simp
-  simp
-  intro x ⟨h₁x, _⟩
-  simp
-
-  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 (AnalyticOn.order.proof_1 h₁f x) h₁x
-
-  --
-  intro x hx
-  simp at hx
-  simp
-  intro h₁x
-  nth_rw 1 [← h₁x] at h₂f
-  tauto
-
-  --
-  rw [Finset.prod_ne_zero_iff]
-  intro x hx
-  simp at hx
-  simp
-  intro h₁x
-  nth_rw 1 [← h₁x] at h₂f
-  tauto
-
-  --
-  simp
-  apply h₂F
-  simp
-
-
-lemma const_mul_circleMap_zero
-  {R θ : ℝ} :
-  circleMap 0 R θ = R * circleMap 0 1 θ := by
-  rw [circleMap_zero, circleMap_zero]
-  simp
-
-
-theorem jensen
-  {R : ℝ}
-  (hR : 0 < R)
-  (f : ℂ → ℂ)
-  (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
-
-
-  let ℓ : ℂ ≃L[ℂ] ℂ :=
-  {
-    toFun := fun x ↦ R * x
-    map_add' := fun x y => DistribSMul.smul_add R x y
-    map_smul' := fun m x => mul_smul_comm m (↑R) x
-    invFun := fun x ↦ R⁻¹ * x
-    left_inv := by
-      intro x
-      simp
-      rw [← mul_assoc, mul_comm, inv_mul_cancel₀, mul_one]
-      simp
-      exact ne_of_gt hR
-    right_inv := by
-      intro x
-      simp
-      rw [← mul_assoc, mul_inv_cancel₀, one_mul]
-      simp
-      exact ne_of_gt hR
-    continuous_toFun := continuous_const_smul R
-    continuous_invFun := continuous_const_smul R⁻¹
-  }
-
-
-  let F := f ∘ ℓ
-
-  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
-
-    intro x hx
-    have : ℓ x = R * x := by rfl
-    rw [this]
-    simp
-    simp at hx
-    rw [abs_of_pos hR]
-    calc R * Complex.abs x
-    _ ≤ R * 1 := by exact (mul_le_mul_iff_of_pos_left hR).mpr hx
-    _ = R := by simp
-
-  have h₂F : F 0 ≠ 0 := by
-    dsimp [F]
-    have : ℓ 0 = R * 0 := by rfl
-    rw [this]
-    simpa
-
-  let A := jensen_case_R_eq_one F h₁F h₂F
-
-  dsimp [F] at A
-  have {x : ℂ} : ℓ x = R * x := by rfl
-  repeat
-    simp_rw [this] at A
-  simp at A
-  simp
-  rw [A]
-  simp_rw [← const_mul_circleMap_zero]
-  simp
-
-  let e : (Metric.closedBall (0 : ℂ) 1) → (Metric.closedBall (0 : ℂ) R) := by
-    intro ⟨x, hx⟩
-    have hy : R • x ∈ Metric.closedBall (0 : ℂ) R := by
-      simp
-      simp at hx
-      have : R = |R| := by exact Eq.symm (abs_of_pos hR)
-      rw [← this]
-      norm_num
-      calc R * Complex.abs x
-      _ ≤ R * 1 := by exact (mul_le_mul_iff_of_pos_left hR).mpr hx
-      _ = R := by simp
-    exact ⟨R • x, hy⟩
-
-  let e' : (Metric.closedBall (0 : ℂ) R) → (Metric.closedBall (0 : ℂ) 1) := by
-    intro ⟨x, hx⟩
-    have hy : R⁻¹ • x ∈ Metric.closedBall (0 : ℂ) 1 := by
-      simp
-      simp at hx
-      have : R = |R| := by exact Eq.symm (abs_of_pos hR)
-      rw [← this]
-      norm_num
-      calc R⁻¹ * Complex.abs x
-      _ ≤ R⁻¹ * R := by
-        apply mul_le_mul_of_nonneg_left hx
-        apply inv_nonneg.mpr
-        exact abs_eq_self.mp (id (Eq.symm this))
-      _ = 1 := by
-        apply inv_mul_cancel₀
-        exact Ne.symm (ne_of_lt hR)
-    exact ⟨R⁻¹ • x, hy⟩
-
-  apply finsum_eq_of_bijective e
-
-
-  apply Function.bijective_iff_has_inverse.mpr
-  use e'
-  constructor
-  · apply Function.leftInverse_iff_comp.mpr
-    funext x
-    dsimp only [e, e',  id_eq, eq_mp_eq_cast, Function.comp_apply]
-    conv =>
-      left
-      arg 1
-      rw [← smul_assoc, smul_eq_mul]
-      rw [inv_mul_cancel₀ (Ne.symm (ne_of_lt hR))]
-      rw [one_smul]
-  · apply Function.rightInverse_iff_comp.mpr
-    funext x
-    dsimp only [e, e',  id_eq, eq_mp_eq_cast, Function.comp_apply]
-    conv =>
-      left
-      arg 1
-      rw [← smul_assoc, smul_eq_mul]
-      rw [mul_inv_cancel₀ (Ne.symm (ne_of_lt hR))]
-      rw [one_smul]
-
-  intro x
-  simp
-  by_cases hx : x = (0 : ℂ)
-  rw [hx]
-  simp
-
-  rw [log_mul, log_mul, log_inv, log_inv]
-  have : R = |R| := by exact Eq.symm (abs_of_pos hR)
-  rw [← this]
-  simp
-  left
-  congr 1
-
-  dsimp [AnalyticOn.order]
-  rw [← AnalyticAt.order_comp_CLE ℓ]
-
-  --
-  simpa
-  --
-  have : R = |R| := by exact Eq.symm (abs_of_pos hR)
-  rw [← this]
-  apply inv_ne_zero
-  exact Ne.symm (ne_of_lt hR)
-  --
-  exact Ne.symm (ne_of_lt hR)
-  --
-  simp
-  constructor
-  · assumption
-  · exact Ne.symm (ne_of_lt hR)

Nevanlinna/holomorphic_examples.lean

@@ -1,314 +0,0 @@
-import Nevanlinna.harmonicAt
-import Nevanlinna.holomorphicAt
-import Nevanlinna.holomorphic_primitive
-import Nevanlinna.mathlibAddOn
-
-
-theorem CauchyRiemann₆
-  {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
-  {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F]
-  {f : E → F}
-  {z : E} :
-  (DifferentiableAt ℂ f z) ↔ (DifferentiableAt ℝ f z) ∧ ∀ e, partialDeriv ℝ (Complex.I • e) f z = Complex.I • partialDeriv ℝ e f z := by
-  constructor
-
-  · -- Direction "→"
-    intro h
-    constructor
-    · exact DifferentiableAt.restrictScalars ℝ h
-    · unfold partialDeriv
-      conv =>
-        intro e
-        left
-        rw [DifferentiableAt.fderiv_restrictScalars ℝ h]
-        simp
-        rw [← mul_one Complex.I]
-        rw [← smul_eq_mul]
-      conv =>
-        intro e
-        right
-        right
-        rw [DifferentiableAt.fderiv_restrictScalars ℝ h]
-      simp
-
-  · -- Direction "←"
-    intro ⟨h₁, h₂⟩
-    apply (differentiableAt_iff_restrictScalars ℝ h₁).2
-
-    use {
-      toFun := fderiv ℝ f z
-      map_add' := fun x y => ContinuousLinearMap.map_add (fderiv ℝ f z) x y
-      map_smul' := by
-        simp
-        intro m x
-        have : m = m.re + m.im • Complex.I := by simp
-        rw [this, add_smul, add_smul, ContinuousLinearMap.map_add]
-        congr
-        simp
-        rw [smul_assoc, smul_assoc, ContinuousLinearMap.map_smul (fderiv ℝ f z) m.2]
-        congr
-        exact h₂ x
-    }
-    rfl
-
-
-theorem CauchyRiemann₇
-  {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F]
-  {f : ℂ → F}
-  {z : ℂ} :
-  (DifferentiableAt ℂ f z) ↔ (DifferentiableAt ℝ f z) ∧ partialDeriv ℝ Complex.I f z = Complex.I • partialDeriv ℝ 1 f z := by
-  constructor
-  · intro hf
-    constructor
-    · exact (CauchyRiemann₆.1 hf).1
-    · let A := (CauchyRiemann₆.1 hf).2 1
-      simp at A
-      exact A
-  · intro ⟨h₁, h₂⟩
-    apply CauchyRiemann₆.2
-    constructor
-    · exact h₁
-    · intro e
-      have : Complex.I • e = e • Complex.I := by
-        rw [smul_eq_mul, smul_eq_mul]
-        exact CommMonoid.mul_comm Complex.I e
-      rw [this]
-      have : e = e.re + e.im • Complex.I := by simp
-      rw [this, add_smul, partialDeriv_add₁, partialDeriv_add₁]
-      simp
-      rw [← smul_eq_mul]
-      have : partialDeriv ℝ ((e.re : ℝ) • Complex.I) f = partialDeriv ℝ ((e.re : ℂ) • Complex.I) f := by rfl
-      rw [← this, partialDeriv_smul₁ ℝ]
-      have : (e.re : ℂ) = (e.re : ℝ) • (1 : ℂ) := by simp
-      rw [this, partialDeriv_smul₁ ℝ]
-      have : partialDeriv ℝ ((e.im : ℂ) * Complex.I) f = partialDeriv ℝ ((e.im : ℝ) • Complex.I) f := by rfl
-      rw [this, partialDeriv_smul₁ ℝ]
-      simp
-      rw [h₂]
-      rw [smul_comm]
-      congr
-      rw [mul_assoc]
-      simp
-      nth_rw 2 [smul_comm]
-      rw [← smul_assoc]
-      simp
-      have : - (e.im : ℂ) = (-e.im : ℝ) • (1 : ℂ) := by simp
-      rw [this, partialDeriv_smul₁ ℝ]
-      simp
-
-
-
-
-/-
-
-A harmonic, real-valued function on ℂ is the real part of a suitable holomorphic
-function.
-
--/
-
-theorem harmonic_is_realOfHolomorphic
-  {f : ℂ → ℝ}
-  {z : ℂ}
-  {R : ℝ}
-  (hR : 0 < R)
-  (hf : ∀ x ∈ Metric.ball z R, HarmonicAt f x) :
-  ∃ F : ℂ → ℂ, (∀ x ∈ Metric.ball z R, HolomorphicAt F x) ∧ (Set.EqOn (Complex.reCLM ∘ F) f (Metric.ball z R)) := by
-
-  let f_1 : ℂ → ℂ := Complex.ofRealCLM ∘ (partialDeriv ℝ 1 f)
-  let f_I : ℂ → ℂ := Complex.ofRealCLM ∘ (partialDeriv ℝ Complex.I f)
-
-  let g : ℂ → ℂ := f_1 - Complex.I • f_I
-
-  have contDiffOn_if_contDiffAt
-    {f' : ℂ → ℝ}
-    {z' : ℂ}
-    {R' : ℝ}
-    {n' : ℕ}
-    (hf' : ∀ x ∈ Metric.ball z' R', ContDiffAt ℝ n' f' x) :
-    ContDiffOn ℝ n' f' (Metric.ball z' R') := by
-    intro z hz
-    apply ContDiffAt.contDiffWithinAt
-    exact hf' z hz
-
-  have reg₂f : ContDiffOn ℝ 2 f (Metric.ball z R) := by
-    apply contDiffOn_if_contDiffAt
-    intro x hx
-    exact (hf x hx).1
-
-  have contDiffOn_if_contDiffAt'
-    {f' : ℂ → ℂ}
-    {z' : ℂ}
-    {R' : ℝ}
-    {n' : ℕ}
-    (hf' : ∀ x ∈ Metric.ball z' R', ContDiffAt ℝ n' f' x) :
-    ContDiffOn ℝ n' f' (Metric.ball z' R') := by
-    intro z hz
-    apply ContDiffAt.contDiffWithinAt
-    exact hf' z hz
-
-  have reg₁f_1 : ContDiffOn ℝ 1 f_1 (Metric.ball z R) := by
-    apply contDiffOn_if_contDiffAt'
-    intro z hz
-    dsimp [f_1]
-    apply ContDiffAt.continuousLinearMap_comp
-    exact partialDeriv_contDiffAt ℝ (hf z hz).1 1
-
-  have reg₁f_I : ContDiffOn ℝ 1 f_I (Metric.ball z R) := by
-    apply contDiffOn_if_contDiffAt'
-    intro z hz
-    dsimp [f_I]
-    apply ContDiffAt.continuousLinearMap_comp
-    exact partialDeriv_contDiffAt ℝ (hf z hz).1 Complex.I
-
-  have reg₁g : ContDiffOn ℝ 1 g (Metric.ball z R) := by
-    dsimp [g]
-    apply ContDiffOn.sub
-    exact reg₁f_1
-    have : Complex.I • f_I = fun x ↦ Complex.I • f_I x := by rfl
-    rw [this]
-    apply ContDiffOn.const_smul
-    exact reg₁f_I
-
-  have reg₁ : DifferentiableOn ℂ g (Metric.ball z R) := by
-    intro x hx
-    apply DifferentiableAt.differentiableWithinAt
-    apply CauchyRiemann₇.2
-    constructor
-    · apply DifferentiableWithinAt.differentiableAt (reg₁g.differentiableOn le_rfl x hx)
-      apply IsOpen.mem_nhds Metric.isOpen_ball hx
-    · dsimp [g]
-      rw [partialDeriv_sub₂_differentiableAt, partialDeriv_sub₂_differentiableAt]
-      dsimp [f_1, f_I]
-      rw [partialDeriv_smul'₂, partialDeriv_smul'₂]
-      rw [partialDeriv_compContLinAt, partialDeriv_compContLinAt]
-      simp
-      rw [partialDeriv_compContLinAt, partialDeriv_compContLinAt]
-      rw [mul_sub]
-      simp
-      rw [← mul_assoc]
-      simp
-      rw [add_comm, sub_eq_add_neg]
-      congr 1
-      · rw [partialDeriv_commOn _ reg₂f Complex.I 1]
-        exact hx
-        exact Metric.isOpen_ball
-      · let A := Filter.EventuallyEq.eq_of_nhds (hf x hx).2
-        simp at A
-        unfold Complex.laplace at A
-        conv =>
-          right
-          right
-          rw [← sub_zero (partialDeriv ℝ 1 (partialDeriv ℝ 1 f) x)]
-          rw [← A]
-        simp
-
-      --DifferentiableAt ℝ (partialDeriv ℝ _ f)
-      repeat
-        apply ContDiffAt.differentiableAt
-        apply partialDeriv_contDiffAt ℝ (hf x hx).1
-        apply le_rfl
-
-      -- DifferentiableAt ℝ f_1 x
-      apply (reg₁f_1.differentiableOn le_rfl).differentiableAt
-      apply IsOpen.mem_nhds Metric.isOpen_ball hx
-
-      -- DifferentiableAt ℝ (Complex.I • f_I)
-      have : Complex.I • f_I = fun x ↦ Complex.I • f_I x := by rfl
-      rw [this]
-      apply DifferentiableAt.const_smul
-      apply (reg₁f_I.differentiableOn le_rfl).differentiableAt
-      apply IsOpen.mem_nhds Metric.isOpen_ball hx
-
-      -- Differentiable ℝ f_1
-      apply (reg₁f_1.differentiableOn le_rfl).differentiableAt
-      apply IsOpen.mem_nhds Metric.isOpen_ball hx
-
-      -- Differentiable ℝ (Complex.I • f_I)
-      have : Complex.I • f_I = fun x ↦ Complex.I • f_I x := by rfl
-      rw [this]
-      apply DifferentiableAt.const_smul
-      apply (reg₁f_I.differentiableOn le_rfl).differentiableAt
-      apply IsOpen.mem_nhds Metric.isOpen_ball hx
-
-  let F := fun z' ↦ (primitive z g) z' + f z
-
-  have regF : DifferentiableOn ℂ F (Metric.ball z R) := by
-    apply DifferentiableOn.add
-    apply primitive_differentiableOn reg₁
-    simp
-
-  have pF'' : ∀ x ∈ Metric.ball z R, (fderiv ℝ F x) = ContinuousLinearMap.lsmul ℝ ℂ (g x) := by
-    intro x hx
-    have : DifferentiableAt ℂ F x := by
-      apply (regF x hx).differentiableAt
-      apply IsOpen.mem_nhds Metric.isOpen_ball hx
-    rw [DifferentiableAt.fderiv_restrictScalars ℝ this]
-    dsimp [F]
-    rw [fderiv_add_const]
-    rw [primitive_fderiv' reg₁ x hx]
-    exact rfl
-
-  use F
-
-  constructor
-  · -- ∀ x ∈ Metric.ball z R, HolomorphicAt F x
-    intro x hx
-    apply HolomorphicAt_iff.2
-    use Metric.ball z R
-    constructor
-    · exact Metric.isOpen_ball
-    · constructor
-      · assumption
-      · intro w hw
-        apply (regF w hw).differentiableAt
-        apply IsOpen.mem_nhds Metric.isOpen_ball hw
-  · -- Set.EqOn (⇑Complex.reCLM ∘ F) f (Metric.ball z R)
-    have : DifferentiableOn ℝ (Complex.reCLM ∘ F) (Metric.ball z R) := by
-      apply DifferentiableOn.comp
-      apply Differentiable.differentiableOn
-      apply ContinuousLinearMap.differentiable Complex.reCLM
-      apply regF.restrictScalars ℝ
-      exact Set.mapsTo'.mpr fun ⦃a⦄ _ => hR
-    have hz : z ∈ Metric.ball z R := by exact Metric.mem_ball_self hR
-    apply Convex.eqOn_of_fderivWithin_eq _ this _ _ _ hz _
-    exact convex_ball z R
-    apply reg₂f.differentiableOn one_le_two
-    apply IsOpen.uniqueDiffOn Metric.isOpen_ball
-
-    intro x hx
-    rw [fderivWithin_eq_fderiv, fderivWithin_eq_fderiv]
-    rw [fderiv.comp]
-    simp
-    apply ContinuousLinearMap.ext
-    intro w
-    simp
-    rw [pF'']
-    dsimp [g, f_1, f_I, partialDeriv]
-    simp
-    have : w = w.re • 1 + w.im • Complex.I := by simp
-    nth_rw 3 [this]
-    rw [(fderiv ℝ f x).map_add]
-    rw [(fderiv ℝ f x).map_smul, (fderiv ℝ f x).map_smul]
-    rw [smul_eq_mul, smul_eq_mul]
-    ring
-
-    assumption
-    exact ContinuousLinearMap.differentiableAt Complex.reCLM
-    apply (regF.restrictScalars ℝ  x hx).differentiableAt
-    apply IsOpen.mem_nhds Metric.isOpen_ball hx
-    apply IsOpen.uniqueDiffOn Metric.isOpen_ball
-    assumption
-    apply (reg₂f.differentiableOn one_le_two).differentiableAt
-    apply IsOpen.mem_nhds Metric.isOpen_ball hx
-    apply IsOpen.uniqueDiffOn Metric.isOpen_ball
-    assumption
-    -- DifferentiableAt ℝ (⇑Complex.reCLM ∘ F) x
-    apply DifferentiableAt.comp
-    apply Differentiable.differentiableAt
-    exact ContinuousLinearMap.differentiable Complex.reCLM
-    apply (regF.restrictScalars ℝ  x hx).differentiableAt
-    apply IsOpen.mem_nhds Metric.isOpen_ball hx
-    --
-    dsimp [F]
-    rw [primitive_zeroAtBasepoint]
-    simp

Nevanlinna/holomorphic_primitive.lean

@@ -1,846 +0,0 @@
-import Mathlib.Analysis.Complex.TaylorSeries
-import Mathlib.Data.ENNReal.Basic
-
-noncomputable def primitive
-  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] :
-  ℂ  → (ℂ → E) → (ℂ → E) := by
-  intro z₀
-  intro f
-  exact fun z ↦ (∫ (x : ℝ) in z₀.re..z.re, f ⟨x, z₀.im⟩) + Complex.I • ∫ (x : ℝ) in z₀.im..z.im, f ⟨z.re, x⟩
-
-
-theorem primitive_zeroAtBasepoint
-  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
-  (f : ℂ  → E)
-  (z₀ : ℂ) :
-  (primitive z₀ f) z₀ = 0 := by
-  unfold primitive
-  simp
-
-
-theorem primitive_fderivAtBasepointZero
-  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
-  {f : ℂ  → E}
-  {R : ℝ}
-  (hR : 0 < R)
-  (hf : ContinuousOn f (Metric.ball 0 R)) :
-  HasDerivAt (primitive 0 f) (f 0) 0 := by
-  unfold primitive
-  simp
-  apply hasDerivAt_iff_isLittleO.2
-  simp
-  rw [Asymptotics.isLittleO_iff]
-  intro c hc
-
-  have {z : ℂ} {e : E} : z • e = (∫ (_ : ℝ) in (0)..(z.re), e) + Complex.I • ∫ (_ : ℝ) in (0)..(z.im), e:= by
-    simp
-    rw [smul_comm]
-    rw [← smul_assoc]
-    simp
-    have : z.re • e = (z.re : ℂ) • e := by exact rfl
-    rw [this, ← add_smul]
-    simp
-  conv =>
-    left
-    intro x
-    left
-    arg 1
-    arg 2
-    rw [this]
-
-  obtain ⟨s, h₁s, h₂s⟩ : ∃ s ⊆ f⁻¹' Metric.ball (f 0) (c / (4 : ℝ)), IsOpen s ∧ 0 ∈ s := by
-    apply eventually_nhds_iff.mp
-    apply continuousAt_def.1
-    apply Continuous.continuousAt
-    fun_prop
-
-    apply continuousAt_def.1
-    apply hf.continuousAt
-    exact Metric.ball_mem_nhds 0 hR
-    apply Metric.ball_mem_nhds (f 0)
-    simpa
-
-  obtain ⟨ε, h₁ε, h₂ε⟩ : ∃ ε > 0, (Metric.ball 0 ε) ×ℂ (Metric.ball 0 ε) ⊆ s ∧ (Metric.ball 0 ε) ×ℂ (Metric.ball 0 ε) ⊆ Metric.ball 0 R := by
-    obtain ⟨ε', h₁ε', h₂ε'⟩ : ∃ ε' > 0, Metric.ball 0 ε' ⊆ s ∩ Metric.ball 0 R := by
-      apply Metric.mem_nhds_iff.mp
-      apply IsOpen.mem_nhds
-      apply IsOpen.inter
-      exact h₂s.1
-      exact Metric.isOpen_ball
-      constructor
-      · exact h₂s.2
-      · simpa
-
-    use (2 : ℝ)⁻¹ * ε'
-
-    constructor
-    · simpa
-    · constructor
-      · intro x hx
-        apply (h₂ε' _).1
-        simp
-        calc Complex.abs x
-        _ ≤ |x.re| + |x.im| := Complex.abs_le_abs_re_add_abs_im x
-        _ < (2 : ℝ)⁻¹ * ε' + |x.im| := by
-          apply (add_lt_add_iff_right |x.im|).mpr
-          have : x.re ∈ Metric.ball 0 (2⁻¹ * ε') := (Complex.mem_reProdIm.1 hx).1
-          simp at this
-          exact this
-        _ < (2 : ℝ)⁻¹ * ε' + (2 : ℝ)⁻¹ * ε' := by
-          apply (add_lt_add_iff_left ((2 : ℝ)⁻¹ * ε')).mpr
-          have : x.im ∈ Metric.ball 0 (2⁻¹ * ε') := (Complex.mem_reProdIm.1 hx).2
-          simp at this
-          exact this
-        _ = ε' := by
-          rw [← add_mul]
-          abel_nf
-          simp
-      · intro x hx
-        apply (h₂ε' _).2
-        simp
-        calc Complex.abs x
-        _ ≤ |x.re| + |x.im| := Complex.abs_le_abs_re_add_abs_im x
-        _ < (2 : ℝ)⁻¹ * ε' + |x.im| := by
-          apply (add_lt_add_iff_right |x.im|).mpr
-          have : x.re ∈ Metric.ball 0 (2⁻¹ * ε') := (Complex.mem_reProdIm.1 hx).1
-          simp at this
-          exact this
-        _ < (2 : ℝ)⁻¹ * ε' + (2 : ℝ)⁻¹ * ε' := by
-          apply (add_lt_add_iff_left ((2 : ℝ)⁻¹ * ε')).mpr
-          have : x.im ∈ Metric.ball 0 (2⁻¹ * ε') := (Complex.mem_reProdIm.1 hx).2
-          simp at this
-          exact this
-        _ = ε' := by
-          rw [← add_mul]
-          abel_nf
-          simp
-
-  have h₃ε : ∀ y ∈ (Metric.ball 0 ε) ×ℂ (Metric.ball 0 ε), ‖(f y) - (f 0)‖ < (c / (4 : ℝ)) := by
-    intro y hy
-    apply mem_ball_iff_norm.mp
-    apply h₁s
-    exact h₂ε.1 hy
-
-
-  have intervalComputation_uIcc {x' y' : ℝ} (h : x' ∈ Set.uIcc 0 y') : |x'| ≤ |y'| := by
-    let A := h.1
-    let B := h.2
-    rcases le_total 0 y' with hy | hy
-    · simp [hy] at A
-      simp [hy] at B
-      rwa [abs_of_nonneg A, abs_of_nonneg hy]
-    · simp [hy] at A
-      simp [hy] at B
-      rw [abs_of_nonpos hy]
-      rw [abs_of_nonpos]
-      linarith [h.1]
-      exact B
-
-
-  rw [Filter.eventually_iff_exists_mem]
-  use Metric.ball 0 (ε / (4 : ℝ))
-
-  constructor
-  · apply Metric.ball_mem_nhds 0
-    linarith
-  · intro y hy
-
-    have {A B C D :E} : (A + B) - (C + D) = (A - C) + (B - D) := by
-      abel
-    rw [this]
-    rw [← smul_sub]
-
-
-    have t₀ : IntervalIntegrable (fun x => f { re := x, im := 0 }) MeasureTheory.volume 0 y.re := by
-      apply ContinuousOn.intervalIntegrable
-      apply ContinuousOn.comp
-      exact hf
-      have : (fun x => ({ re := x, im := 0 } : ℂ)) = Complex.ofRealLI := by rfl
-      rw [this]
-      apply Continuous.continuousOn
-      continuity
-      intro x hx
-      apply h₂ε.2
-      simp
-      constructor
-      · simp
-        calc |x|
-        _ ≤ |y.re| := by apply intervalComputation_uIcc hx
-        _ ≤ Complex.abs y := by exact Complex.abs_re_le_abs y
-        _ < ε / 4 := by simp at hy; assumption
-        _ < ε := by linarith
-      · simpa
-    have t₁ : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 y.re := by
-      apply ContinuousOn.intervalIntegrable
-      apply ContinuousOn.comp
-      apply hf
-      fun_prop
-      intro x _
-      simpa
-    rw [← intervalIntegral.integral_sub t₀ t₁]
-
-    have t₂ : IntervalIntegrable (fun x_1 => f { re := y.re, im := x_1 }) MeasureTheory.volume 0 y.im := by
-      apply ContinuousOn.intervalIntegrable
-      apply ContinuousOn.comp
-      exact hf
-      have : (Complex.mk y.re) = (fun x => Complex.I • Complex.ofRealCLM x + { re := y.re, im := 0 }) := by
-        funext x
-        apply Complex.ext
-        rw [Complex.add_re]
-        simp
-        simp
-      rw [this]
-      apply ContinuousOn.add
-      apply Continuous.continuousOn
-      continuity
-      fun_prop
-      intro x hx
-      apply h₂ε.2
-      constructor
-      · simp
-        calc |y.re|
-        _ ≤ Complex.abs y := by exact Complex.abs_re_le_abs y
-        _ < ε / 4 := by simp at hy; assumption
-        _ < ε := by linarith
-      · simp
-        calc |x|
-        _ ≤ |y.im| := by apply intervalComputation_uIcc hx
-        _ ≤ Complex.abs y := by exact Complex.abs_im_le_abs y
-        _ < ε / 4 := by simp at hy; assumption
-        _ < ε := by linarith
-    have t₃ : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 y.im := by
-      apply ContinuousOn.intervalIntegrable
-      apply ContinuousOn.comp
-      exact hf
-      fun_prop
-      intro x _
-      apply h₂ε.2
-      simp
-      constructor
-      · simpa
-      · simpa
-    rw [← intervalIntegral.integral_sub t₂ t₃]
-
-    have h₁y : |y.re| < ε / 4 := by
-      calc |y.re|
-      _ ≤ Complex.abs y := by apply Complex.abs_re_le_abs
-      _ < ε / 4 := by
-        let A := mem_ball_iff_norm.1 hy
-        simp at A
-        linarith
-    have h₂y : |y.im| < ε / 4 := by
-      calc |y.im|
-      _ ≤ Complex.abs y := by apply Complex.abs_im_le_abs
-      _ < ε / 4 := by
-        let A := mem_ball_iff_norm.1 hy
-        simp at A
-        linarith
-
-    have intervalComputation {x' y' : ℝ} (h : x' ∈ Ι 0 y') : |x'| ≤ |y'| := by
-      let A := h.1
-      let B := h.2
-      rcases le_total 0 y' with hy | hy
-      · simp [hy] at A
-        simp [hy] at B
-        rw [abs_of_nonneg hy]
-        rw [abs_of_nonneg (le_of_lt A)]
-        exact B
-      · simp [hy] at A
-        simp [hy] at B
-        rw [abs_of_nonpos hy]
-        rw [abs_of_nonpos]
-        linarith [h.1]
-        exact B
-
-    have t₁ : ‖(∫ (x : ℝ) in (0)..(y.re), f { re := x, im := 0 } - f 0)‖ ≤ (c / (4 : ℝ)) * |y.re - 0| := by
-      apply intervalIntegral.norm_integral_le_of_norm_le_const
-      intro x hx
-
-      have h₁x : |x| < ε / 4 := by
-        calc |x|
-          _ ≤ |y.re| := intervalComputation hx
-          _ < ε / 4 := h₁y
-      apply le_of_lt
-      apply h₃ε { re := x, im := 0 }
-      constructor
-      · simp
-        linarith
-      · simp
-        exact h₁ε
-
-    have t₂ : ‖∫ (x : ℝ) in (0)..(y.im), f { re := y.re, im := x } - f 0‖ ≤ (c / (4 : ℝ)) * |y.im - 0| := by
-      apply intervalIntegral.norm_integral_le_of_norm_le_const
-      intro x hx
-
-      have h₁x : |x| < ε / 4 := by
-        calc |x|
-          _ ≤ |y.im| := intervalComputation hx
-          _ < ε / 4 := h₂y
-
-      apply le_of_lt
-      apply h₃ε { re := y.re, im := x }
-      constructor
-      · simp
-        linarith
-      · simp
-        linarith
-
-    calc ‖(∫ (x : ℝ) in (0)..(y.re), f { re := x, im := 0 } - f 0) + Complex.I • ∫ (x : ℝ) in (0)..(y.im), f { re := y.re, im := x } - f 0‖
-      _ ≤ ‖(∫ (x : ℝ) in (0)..(y.re), f { re := x, im := 0 } - f 0)‖ + ‖Complex.I • ∫ (x : ℝ) in (0)..(y.im), f { re := y.re, im := x } - f 0‖ := by
-        apply norm_add_le
-      _ ≤ ‖(∫ (x : ℝ) in (0)..(y.re), f { re := x, im := 0 } - f 0)‖ + ‖∫ (x : ℝ) in (0)..(y.im), f { re := y.re, im := x } - f 0‖ := by
-        simp
-        rw [norm_smul]
-        simp
-      _ ≤ (c / (4 : ℝ)) * |y.re - 0| + (c / (4 : ℝ)) * |y.im - 0| := by
-        apply add_le_add
-        exact t₁
-        exact t₂
-      _ ≤ (c / (4 : ℝ)) * (|y.re| + |y.im|) := by
-        simp
-        rw [mul_add]
-      _ ≤ (c / (4 : ℝ)) * (4 * ‖y‖) := by
-        have : |y.re| + |y.im| ≤ 4 * ‖y‖ := by
-          calc |y.re| + |y.im|
-            _ ≤ ‖y‖ + ‖y‖ := by
-              apply add_le_add
-              apply Complex.abs_re_le_abs
-              apply Complex.abs_im_le_abs
-            _ ≤ 4 * ‖y‖ := by
-              rw [← two_mul]
-              apply mul_le_mul
-              linarith
-              rfl
-              exact norm_nonneg y
-              linarith
-
-        apply mul_le_mul
-        rfl
-        exact this
-        apply add_nonneg
-        apply abs_nonneg
-        apply abs_nonneg
-        linarith
-      _ ≤ c * ‖y‖ := by
-        linarith
-
-
-theorem primitive_translation
-  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
-  (f : ℂ  → E)
-  (z₀ t : ℂ) :
-  primitive z₀ (f ∘ fun z ↦ (z - t)) = ((primitive (z₀ - t) f) ∘ fun z ↦ (z - t)) := by
-  funext z
-  unfold primitive
-  simp
-
-  let g : ℝ → E := fun x ↦ f ( {re := x, im := z₀.im - t.im} )
-  have {x : ℝ} : f ({ re := x, im := z₀.im } - t) = g (1*x - t.re) := by
-    congr 1
-    apply Complex.ext <;> simp
-  conv =>
-    left
-    left
-    arg 1
-    intro x
-    rw [this]
-  rw [intervalIntegral.integral_comp_mul_sub g one_ne_zero (t.re)]
-  simp
-
-  congr 1
-  let g : ℝ → E := fun x ↦ f ( {re := z.re - t.re, im := x} )
-  have {x : ℝ} : f ({ re := z.re, im := x} - t) = g (1*x - t.im) := by
-    congr 1
-    apply Complex.ext <;> simp
-  conv =>
-    left
-    arg 1
-    intro x
-    rw [this]
-  rw [intervalIntegral.integral_comp_mul_sub g one_ne_zero (t.im)]
-  simp
-
-
-theorem primitive_hasDerivAtBasepoint
-  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
-  {f : ℂ  → E}
-  {R : ℝ}
-  (z₀ : ℂ)
-  (hR : 0 < R)
-  (hf : ContinuousOn f (Metric.ball z₀ R)) :
-  HasDerivAt (primitive z₀ f) (f z₀) z₀ := by
-
-  let g := f ∘ fun z ↦ z + z₀
-  have hg : ContinuousOn g (Metric.ball 0 R) := by
-    apply ContinuousOn.comp
-    fun_prop
-    fun_prop
-    intro x hx
-    simp
-    simp at hx
-    assumption
-
-  let B := primitive_translation g z₀ z₀
-  simp at B
-  have : (g ∘ fun z ↦ (z - z₀)) = f := by
-    funext z
-    dsimp [g]
-    simp
-  rw [this] at B
-  rw [B]
-  have : f z₀ = (1 : ℂ) • (f z₀) := (MulAction.one_smul (f z₀)).symm
-  conv =>
-    arg 2
-    rw [this]
-
-  apply HasDerivAt.scomp
-  simp
-  have : g 0 = f z₀ := by simp [g]
-  rw [← this]
-  exact primitive_fderivAtBasepointZero hR hg
-  apply HasDerivAt.sub_const
-  have : (fun (x : ℂ) ↦ x) = id := by
-    funext x
-    simp
-  rw [this]
-  exact hasDerivAt_id z₀
-
-
-theorem primitive_additivity
-  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
-  {f : ℂ  → E}
-  {z₀ : ℂ}
-  {rx ry : ℝ}
-  (hf : DifferentiableOn ℂ f (Metric.ball z₀.re rx ×ℂ Metric.ball z₀.im ry))
-  (hry : 0 < ry)
-  {z₁ : ℂ}
-  (hz₁ : z₁ ∈ (Metric.ball z₀.re rx ×ℂ Metric.ball z₀.im ry))
-  :
-  ∃ εx > 0, ∃ εy > 0, ∀ z ∈ (Metric.ball z₁.re εx ×ℂ Metric.ball z₁.im εy), (primitive z₀ f z) - (primitive z₁ f z) - (primitive z₀ f z₁) = 0 := by
-
-  let εx := rx - dist z₀.re z₁.re
-  have hεx : εx > 0 := by
-    let A := hz₁.1
-    simp at A
-    dsimp [εx]
-    rw [dist_comm]
-    simpa
-  let εy := ry - dist z₀.im z₁.im
-  have hεy : εy > 0 := by
-    let A := hz₁.2
-    simp at A
-    dsimp [εy]
-    rw [dist_comm]
-    simpa
-
-  use εx
-  use hεx
-  use εy
-  use hεy
-
-  intro z hz
-
-  unfold primitive
-
-  have : (∫ (x : ℝ) in z₀.re..z.re, f { re := x, im := z₀.im }) = (∫ (x : ℝ) in z₀.re..z₁.re, f { re := x, im := z₀.im }) + (∫ (x : ℝ) in z₁.re..z.re, f { re := x, im := z₀.im }) := by
-
-    rw [intervalIntegral.integral_add_adjacent_intervals]
-
-    -- IntervalIntegrable (fun x => f { re := x, im := z₀.im }) MeasureTheory.volume z₀.re z₁.re
-    apply ContinuousOn.intervalIntegrable
-    apply ContinuousOn.comp
-    exact hf.continuousOn
-    have {b : ℝ} : ((fun x => { re := x, im := b }) : ℝ → ℂ) = (fun x => Complex.ofRealCLM x + { re := 0, im := b }) := by
-      funext x
-      apply Complex.ext
-      rw [Complex.add_re]
-      simp
-      rw [Complex.add_im]
-      simp
-    apply Continuous.continuousOn
-    rw [this]
-    continuity
-    -- Remains: Set.MapsTo (fun x => { re := x, im := z₀.im }) (Set.uIcc z₀.re z₁.re) (Metric.ball z₀.re rx ×ℂ Metric.ball z₀.im ry)
-    intro w hw
-    simp
-    apply Complex.mem_reProdIm.mpr
-    constructor
-    · simp
-      calc dist w z₀.re
-      _ ≤ dist z₁.re z₀.re := by apply Real.dist_right_le_of_mem_uIcc; rwa [Set.uIcc_comm] at hw
-      _ < rx := by apply Metric.mem_ball.mp (Complex.mem_reProdIm.1 hz₁).1
-    · simpa
-
-    -- IntervalIntegrable (fun x => f { re := x, im := z₀.im }) MeasureTheory.volume z₁.re z.re
-    apply ContinuousOn.intervalIntegrable
-    apply ContinuousOn.comp
-    exact hf.continuousOn
-    have {b : ℝ} : ((fun x => { re := x, im := b }) : ℝ → ℂ) = (fun x => Complex.ofRealCLM x + { re := 0, im := b }) := by
-      funext x
-      apply Complex.ext
-      rw [Complex.add_re]
-      simp
-      rw [Complex.add_im]
-      simp
-    apply Continuous.continuousOn
-    rw [this]
-    continuity
-    -- Remains: Set.MapsTo (fun x => { re := x, im := z₀.im }) (Set.uIcc z₁.re z.re) (Metric.ball z₀.re rx ×ℂ Metric.ball z₀.im ry)
-    intro w hw
-    simp
-    constructor
-    · simp
-      calc dist w z₀.re
-      _ ≤ dist w z₁.re + dist z₁.re z₀.re := by exact dist_triangle w z₁.re z₀.re
-      _ ≤ dist z.re z₁.re + dist z₁.re z₀.re := by
-        apply (add_le_add_iff_right (dist z₁.re z₀.re)).mpr
-        rw [Set.uIcc_comm] at hw
-        exact Real.dist_right_le_of_mem_uIcc hw
-      _ < (rx - dist z₀.re z₁.re) + dist z₁.re z₀.re := by
-        apply (add_lt_add_iff_right (dist z₁.re z₀.re)).mpr
-        apply Metric.mem_ball.1 (Complex.mem_reProdIm.1 hz).1
-      _ = rx := by
-        rw [dist_comm]
-        simp
-    · simpa
-  rw [this]
-
-  have : (∫ (x : ℝ) in z₀.im..z.im, f { re := z.re, im := x }) = (∫ (x : ℝ) in z₀.im..z₁.im, f { re := z.re, im := x }) + (∫ (x : ℝ) in z₁.im..z.im, f { re := z.re, im := x }) := by
-    rw [intervalIntegral.integral_add_adjacent_intervals]
-
-    -- IntervalIntegrable (fun x => f { re := z.re, im := x }) MeasureTheory.volume z₀.im z₁.im
-    apply ContinuousOn.intervalIntegrable
-    apply ContinuousOn.comp
-    exact hf.continuousOn
-    apply Continuous.continuousOn
-    have {b : ℝ}:  (Complex.mk b) = (fun x => Complex.I • Complex.ofRealCLM x + { re := b, im := 0 }) := by
-      funext x
-      apply Complex.ext
-      rw [Complex.add_re]
-      simp
-      simp
-    rw [this]
-    apply Continuous.add
-    fun_prop
-    fun_prop
-    -- Set.MapsTo (Complex.mk z.re) (Set.uIcc z₀.im z₁.im) (Metric.ball z₀.re rx ×ℂ Metric.ball z₀.im ry)
-    intro w hw
-    constructor
-    · simp
-      calc dist z.re z₀.re
-      _ ≤ dist z.re z₁.re + dist z₁.re z₀.re := by exact dist_triangle z.re z₁.re z₀.re
-      _ < (rx - dist z₀.re z₁.re) + dist z₁.re z₀.re := by
-        apply (add_lt_add_iff_right (dist z₁.re z₀.re)).mpr
-        apply Metric.mem_ball.1 (Complex.mem_reProdIm.1 hz).1
-      _ = rx := by
-        rw [dist_comm]
-        simp
-    · simp
-      calc dist w z₀.im
-      _ ≤ dist z₁.im z₀.im := by rw [Set.uIcc_comm] at hw; exact Real.dist_right_le_of_mem_uIcc hw
-      _ < ry := by
-        rw [← Metric.mem_ball]
-        exact hz₁.2
-
-    -- IntervalIntegrable (fun x => f { re := z.re, im := x }) MeasureTheory.volume z₁.im z.im
-    apply ContinuousOn.intervalIntegrable
-    apply ContinuousOn.comp
-    exact hf.continuousOn
-    apply Continuous.continuousOn
-    have {b : ℝ}:  (Complex.mk b) = (fun x => Complex.I • Complex.ofRealCLM x + { re := b, im := 0 }) := by
-      funext x
-      apply Complex.ext
-      rw [Complex.add_re]
-      simp
-      simp
-    rw [this]
-    apply Continuous.add
-    fun_prop
-    fun_prop
-    -- Set.MapsTo (Complex.mk z.re) (Set.uIcc z₁.im z.im) (Metric.ball z₀.re rx ×ℂ Metric.ball z₀.im ry)
-    intro w hw
-    constructor
-    · simp
-      calc dist z.re z₀.re
-      _ ≤ dist z.re z₁.re + dist z₁.re z₀.re := by exact dist_triangle z.re z₁.re z₀.re
-      _ < (rx - dist z₀.re z₁.re) + dist z₁.re z₀.re := by
-        apply (add_lt_add_iff_right (dist z₁.re z₀.re)).mpr
-        apply Metric.mem_ball.1 (Complex.mem_reProdIm.1 hz).1
-      _ = rx := by
-        rw [dist_comm]
-        simp
-    · simp
-      calc dist w z₀.im
-      _ ≤ dist w z₁.im + dist z₁.im z₀.im := by exact dist_triangle w z₁.im z₀.im
-      _ ≤ dist z.im z₁.im + dist z₁.im z₀.im := by
-        apply (add_le_add_iff_right (dist z₁.im z₀.im)).mpr
-        rw [Set.uIcc_comm] at hw
-        exact Real.dist_right_le_of_mem_uIcc hw
-      _ < (ry - dist z₀.im z₁.im) + dist z₁.im z₀.im := by
-        apply (add_lt_add_iff_right (dist z₁.im z₀.im)).mpr
-        apply Metric.mem_ball.1 (Complex.mem_reProdIm.1 hz).2
-      _ = ry := by
-        rw [dist_comm]
-        simp
-  rw [this]
-
-  simp
-
-  have {a b c d e f g h : E} : (a + b) + (c + d) - (e + f) - (g + h) = b + (a - g) - e - f + d  - h + (c) := by
-    abel
-  rw [this]
-
-
-  have H' : DifferentiableOn ℂ f (Set.uIcc z₁.re z.re ×ℂ Set.uIcc z₀.im z₁.im) := by
-    apply DifferentiableOn.mono hf
-    intro x hx
-    constructor
-    · simp
-      calc dist x.re z₀.re
-      _ ≤ dist x.re z₁.re + dist z₁.re z₀.re := by exact dist_triangle x.re z₁.re z₀.re
-      _ ≤ dist z.re z₁.re + dist z₁.re z₀.re := by
-        apply (add_le_add_iff_right (dist z₁.re z₀.re)).mpr
-        rw [Set.uIcc_comm] at hx
-        apply Real.dist_right_le_of_mem_uIcc (Complex.mem_reProdIm.1 hx).1
-      _ < (rx - dist z₀.re z₁.re) + dist z₁.re z₀.re := by
-        apply (add_lt_add_iff_right (dist z₁.re z₀.re)).mpr
-        apply Metric.mem_ball.1 (Complex.mem_reProdIm.1 hz).1
-      _ = rx := by
-        rw [dist_comm]
-        simp
-    · simp
-      calc dist x.im z₀.im
-      _ ≤ dist z₀.im z₁.im := by rw [dist_comm]; exact Real.dist_left_le_of_mem_uIcc (Complex.mem_reProdIm.1 hx).2
-      _ < ry := by
-        rw [dist_comm]
-        exact Metric.mem_ball.1 (Complex.mem_reProdIm.1 hz₁).2
-
-  let A := Complex.integral_boundary_rect_eq_zero_of_differentiableOn f ⟨z₁.re, z₀.im⟩ ⟨z.re, z₁.im⟩ H'
-  have {x : ℝ} {w : ℂ} : ↑x + w.im * Complex.I = { re := x, im := w.im } := by
-    apply Complex.ext
-    · simp
-    · simp
-  simp_rw [this] at A
-  have {x : ℝ} {w : ℂ} : w.re + x * Complex.I = { re := w.re, im := x } := by
-    apply Complex.ext
-    · simp
-    · simp
-  simp_rw [this] at A
-  rw [← A]
-  abel
-
-
-theorem primitive_additivity'
-  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
-  {f : ℂ  → E}
-  {z₀ z₁ : ℂ}
-  {R : ℝ}
-  (hf : DifferentiableOn ℂ f (Metric.ball z₀ R))
-  (hz₁ : z₁ ∈ Metric.ball z₀ R)
-  :
-  primitive z₀ f =ᶠ[nhds z₁] fun z ↦ (primitive z₁ f z) + (primitive z₀ f z₁) := by
-
-  let d := fun ε ↦ √((dist z₁.re z₀.re + ε) ^ 2 + (dist z₁.im z₀.im + ε) ^ 2)
-  have h₀d : Continuous d := by continuity
-  have h₁d : ∀ ε, 0 ≤ d ε := fun ε ↦ Real.sqrt_nonneg ((dist z₁.re z₀.re + ε) ^ 2 + (dist z₁.im z₀.im + ε) ^ 2)
-
-  obtain ⟨ε, h₀ε, h₁ε⟩ : ∃ ε > 0, d ε < R := by
-    let Omega := d⁻¹' Metric.ball 0 R
-
-    have lem₀Ω : IsOpen Omega := IsOpen.preimage h₀d Metric.isOpen_ball
-    have lem₁Ω : 0 ∈ Omega := by
-      dsimp [Omega, d]; simp
-      have : dist z₁.re z₀.re = |z₁.re - z₀.re| := by exact rfl
-      rw [this]
-      have : dist z₁.im z₀.im = |z₁.im - z₀.im| := by exact rfl
-      rw [this]
-      simp
-      rw [← Complex.dist_eq_re_im]; simp
-      exact hz₁
-    obtain ⟨ε, h₁ε, h₂ε⟩ := Metric.isOpen_iff.1 lem₀Ω 0 lem₁Ω
-
-    let ε' := (2 : ℝ)⁻¹ * ε
-
-    have h₀ε' : ε' ∈ Omega := by
-      apply h₂ε
-      dsimp [ε']; simp
-      have : |ε| = ε := by apply abs_of_pos h₁ε
-      rw [this]
-      apply (inv_mul_lt_iff zero_lt_two).mpr
-      linarith
-    have h₁ε' : 0 < ε' := by
-      apply mul_pos _ h₁ε
-      apply inv_pos.mpr
-      exact zero_lt_two
-
-    use ε'
-
-    constructor
-    · exact h₁ε'
-    · dsimp [Omega] at h₀ε'; simp at h₀ε'
-      rwa [abs_of_nonneg (h₁d ε')] at h₀ε'
-
-  let rx := dist z₁.re z₀.re + ε
-  let ry := dist z₁.im z₀.im + ε
-
-  have h'ry : 0 < ry := by
-    dsimp [ry]
-    apply add_pos_of_nonneg_of_pos
-    exact dist_nonneg
-    simpa
-
-  have h'f : DifferentiableOn ℂ f (Metric.ball z₀.re rx ×ℂ Metric.ball z₀.im ry) := by
-    apply hf.mono
-    intro x hx
-    simp
-    rw [Complex.dist_eq_re_im]
-
-    have t₀ : dist x.re z₀.re < rx := Metric.mem_ball.mp hx.1
-    have t₁ : dist x.im z₀.im < ry := Metric.mem_ball.mp hx.2
-    have t₂ : √((x.re - z₀.re) ^ 2 + (x.im - z₀.im) ^ 2) < √( rx ^ 2 + ry ^ 2) := by
-      rw [Real.sqrt_lt_sqrt_iff]
-      apply add_lt_add
-      · rw [sq_lt_sq]
-        dsimp [dist] at t₀
-        nth_rw 2 [abs_of_nonneg]
-        assumption
-        apply add_nonneg dist_nonneg (le_of_lt h₀ε)
-      · rw [sq_lt_sq]
-        dsimp [dist] at t₁
-        nth_rw 2 [abs_of_nonneg]
-        assumption
-        apply add_nonneg dist_nonneg (le_of_lt h₀ε)
-      apply add_nonneg
-      exact sq_nonneg (x.re - z₀.re)
-      exact sq_nonneg (x.im - z₀.im)
-
-    calc √((x.re - z₀.re) ^ 2 + (x.im - z₀.im) ^ 2)
-    _ < √( rx ^ 2 + ry ^ 2) := by
-      exact t₂
-    _ = d ε := by dsimp [d, rx, ry]
-    _ < R := by exact h₁ε
-
-  have h'z₁ : z₁ ∈ (Metric.ball z₀.re rx ×ℂ Metric.ball z₀.im ry) := by
-    dsimp [rx, ry]
-    constructor
-    · simp; exact h₀ε
-    · simp; exact h₀ε
-
-  obtain ⟨εx, hεx, εy, hεy, hε⟩ := primitive_additivity h'f h'ry h'z₁
-
-  apply Filter.eventuallyEq_iff_exists_mem.2
-  use (Metric.ball z₁.re εx ×ℂ Metric.ball z₁.im εy)
-  constructor
-  · apply IsOpen.mem_nhds
-    apply IsOpen.reProdIm
-    exact Metric.isOpen_ball
-    exact Metric.isOpen_ball
-    constructor
-    · simpa
-    · simpa
-  · intro x hx
-    simp
-    rw [← sub_zero (primitive z₀ f x), ← hε x hx]
-    abel
-
-
-theorem primitive_hasDerivAt
-  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
-  {f : ℂ  → E}
-  {z₀ z : ℂ}
-  {R : ℝ}
-  (hf : DifferentiableOn ℂ f (Metric.ball z₀ R))
-  (hz : z ∈ Metric.ball z₀ R) :
-  HasDerivAt (primitive z₀ f) (f z) z := by
-
-  let A := primitive_additivity' hf hz
-  rw [Filter.EventuallyEq.hasDerivAt_iff A]
-  rw [← add_zero (f z)]
-  apply HasDerivAt.add
-
-  let R' := R - dist z z₀
-  have h₀R' : 0 < R' := by
-    dsimp [R']
-    simp
-    exact hz
-  have h₁R' : Metric.ball z R' ⊆ Metric.ball z₀ R := by
-    intro x hx
-    simp
-    calc dist x z₀
-    _ ≤ dist x z + dist z z₀ := dist_triangle x z z₀
-    _ < R' + dist z z₀ := by
-      refine add_lt_add_right ?bc (dist z z₀)
-      exact hx
-    _ = R := by
-      dsimp [R']
-      simp
-
-  apply primitive_hasDerivAtBasepoint
-  exact h₀R'
-  apply ContinuousOn.mono hf.continuousOn h₁R'
-  apply hasDerivAt_const
-
-
-theorem primitive_differentiableOn
-  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
-  {f : ℂ  → E}
-  {z₀ : ℂ}
-  {R : ℝ}
-  (hf : DifferentiableOn ℂ f (Metric.ball z₀ R))
-  :
-  DifferentiableOn ℂ (primitive z₀ f) (Metric.ball z₀ R) := by
-  intro z hz
-  apply DifferentiableAt.differentiableWithinAt
-  exact (primitive_hasDerivAt hf hz).differentiableAt
-
-
-theorem primitive_hasFderivAt
-  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
-  {f : ℂ  → E}
-  (z₀ : ℂ)
-  (R : ℝ)
-  (hf : DifferentiableOn ℂ f (Metric.ball z₀ R))
-  :
-  ∀ z ∈ Metric.ball z₀ R, HasFDerivAt (primitive z₀ f) ((ContinuousLinearMap.lsmul ℂ ℂ).flip (f z)) z := by
-  intro z hz
-  rw [hasFDerivAt_iff_hasDerivAt]
-  simp
-  apply primitive_hasDerivAt hf hz
-
-
-theorem primitive_hasFderivAt'
-  {f : ℂ  → ℂ}
-  {z₀ : ℂ}
-  {R : ℝ}
-  (hf : DifferentiableOn ℂ f (Metric.ball z₀ R))
-  :
-  ∀ z ∈ Metric.ball z₀ R, HasFDerivAt (primitive z₀ f) (ContinuousLinearMap.lsmul ℂ ℂ (f z)) z := by
-  intro z hz
-  rw [hasFDerivAt_iff_hasDerivAt]
-  simp
-  exact primitive_hasDerivAt hf hz
-
-
-theorem primitive_fderiv
-  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
-  {f : ℂ  → E}
-  {z₀ : ℂ}
-  {R : ℝ}
-  (hf : DifferentiableOn ℂ f (Metric.ball z₀ R))
-  :
-  ∀ z ∈ Metric.ball z₀ R, (fderiv ℂ (primitive z₀ f) z) = (ContinuousLinearMap.lsmul ℂ ℂ).flip (f z) := by
-  intro z hz
-  apply HasFDerivAt.fderiv
-  exact primitive_hasFderivAt z₀ R hf z hz
-
-
-theorem primitive_fderiv'
-  {f : ℂ  → ℂ}
-  {z₀ : ℂ}
-  {R : ℝ}
-  (hf : DifferentiableOn ℂ f (Metric.ball z₀ R))
-  :
-  ∀ z ∈ Metric.ball z₀ R, (fderiv ℂ (primitive z₀ f) z) = ContinuousLinearMap.lsmul ℂ ℂ (f z) := by
-  intro z hz
-  apply HasFDerivAt.fderiv
-  exact primitive_hasFderivAt' hf z hz

Nevanlinna/holomorphic_zero.lean

@@ -1,358 +0,0 @@
-import Init.Classical
-import Mathlib.Analysis.Analytic.Meromorphic
-import Mathlib.Topology.ContinuousOn
-import Mathlib.Analysis.Analytic.IsolatedZeros
-import Nevanlinna.holomorphic
-import Nevanlinna.analyticOn_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]
-
-
-theorem zeroDivisor_eq_ord_AtZeroDivisorSupport'
-  {f : ℂ → ℂ}
-  {z : ℂ}
-  (h : z ∈ Function.support (zeroDivisor f)) :
-  zeroDivisor f z = (analyticAtZeroDivisorSupport h).order := by
-
-  unfold zeroDivisor
-  simp [analyticAtZeroDivisorSupport h]
-  sorry
-
-
-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 : AnalyticOn ℂ 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 := AnalyticOn.eqOn_zero_of_preconnected_of_frequently_eq_zero h₁f hU z' hz'
-  tauto
-
-
-theorem supportZeroSet
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  (hU : IsPreconnected U)
-  (h₁f : AnalyticOn ℂ 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
-
-
-theorem discreteZeros
-  {f : ℂ → ℂ} :
-  DiscreteTopology (Function.support (zeroDivisor f)) := by
-
-  simp_rw [← singletons_open_iff_discrete, Metric.isOpen_singleton_iff]
-  intro z
-
-  have A : zeroDivisor f ↑z ≠ 0 := by exact z.2
-  let B := zeroDivisor_eq_ord_AtZeroDivisorSupport z.2
-  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 z.2) m
-  rw [E] at hm
-
-  obtain ⟨g, h₁g, h₂g, h₃g⟩ := hm
-
-  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 ε₁ ε₂
-
-  let F := h₂ε₂ y.1 h₂y
-  rw [zeroDivisor_zeroSet y.2] at F
-  simp at F
-
-  simp [h₂m] at F
-
-  have : g y.1 ≠ 0 := by
-    exact h₁ε₁.2 y h₃y
-  simp [this] at F
-  ext
-  rwa [sub_eq_zero] at F
-
-
-theorem zeroDivisor_finiteOnCompact
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  (hU : IsPreconnected 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
-
-  have hinter : IsCompact (U ∩ Function.support (zeroDivisor f)) := by
-    apply IsCompact.of_isClosed_subset h₂U
-    rw [supportZeroSet]
-    apply h₁f.continuousOn.preimage_isClosed_of_isClosed
-    exact IsCompact.isClosed h₂U
-    exact isClosed_singleton
-    assumption
-    assumption
-    assumption
-    exact Set.inter_subset_left
-
-  apply hinter.finite
-  apply DiscreteTopology.of_subset (s := Function.support (zeroDivisor f))
-  exact discreteZeros (f := f)
-  exact Set.inter_subset_right
-
-
-
-
-noncomputable def zeroDivisorDegree
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  (h₁U : IsPreconnected U) -- not needed!
-  (h₂U : IsCompact 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
-
-
-lemma zeroDivisorDegreeZero
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  (h₁U : IsPreconnected U) -- not needed!
-  (h₂U : IsCompact 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
-
-
-lemma eliminatingZeros₀
-  {U : Set ℂ}
-  (h₁U : IsPreconnected U)
-  (h₂U : IsCompact U) :
-  ∀ 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 : ℂ → ℂ, (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
-  -- case zero
-  intro f h₁f h₂f h₃f
-  use f
-  rw [zeroDivisorDegreeZero] at h₃f
-  rw [h₃f]
-  simpa
-
-  -- case succ
-  intro f h₁f h₂f h₃f
-
-  let Supp := (zeroDivisor_finiteOnCompact h₁U h₁f h₂f h₂U).toFinset
-
-  have : Supp.Nonempty := by
-    rw [← Finset.one_le_card]
-    calc 1
-    _ ≤ n + 1 := by exact Nat.le_add_left 1 n
-    _ = zeroDivisorDegree h₁U h₂U h₁f h₂f := by exact h₃f
-    _ = Supp.card := by rfl
-  obtain ⟨z₀, hz₀⟩ := this
-  dsimp [Supp] at hz₀
-  simp only [Set.Finite.mem_toFinset, Set.mem_inter_iff] at hz₀
-
-
-
-
-  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
-  let C := A B
-  obtain ⟨g₀, h₁g₀, h₂g₀, h₃g₀⟩ := C
-
-  have h₄g₀ : ∃ z ∈ U, g₀ z ≠ 0 := by sorry
-  have h₅g₀ : n = zeroDivisorDegree h₁U h₂U h₁g₀ h₄g₀ := by sorry
-
-  obtain ⟨F, h₁F, h₂F⟩ := ih g₀ h₁g₀ h₄g₀ h₅g₀
-  use F
-  constructor
-  · assumption
-  ·
-    sorry

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
-    apply A₀.differentiableAt (Preorder.le_refl 1)
+    exact A₀.differentiableAt (Submonoid.oneLE.proof_2 ℕ∞)
   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 (Preorder.le_refl 1)
+    exact A₀.differentiableAt (Submonoid.oneLE.proof_2 ℕ∞)
   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 (Preorder.le_refl 1)
+    exact A₀.differentiableAt (Submonoid.oneLE.proof_2 ℕ∞)
   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 (Preorder.le_refl 1)
+    exact A₀.differentiableAt (Submonoid.oneLE.proof_2 ℕ∞)
   rw [partialDeriv_add₂_differentiableAt ℝ t₃ t₄]
 
   -- I am super confused at this point because the tactic 'ring' does not work.

Nevanlinna/laplace2.lean

@@ -4,12 +4,21 @@ import Mathlib.Analysis.InnerProductSpace.PiL2
 --import Mathlib.Algebra.BigOperators.Basic
 import Mathlib.Analysis.Calculus.ContDiff.Bounds
 import Mathlib.Analysis.Calculus.FDeriv.Symmetric
---import Mathlib.LinearAlgebra.Basis
---import Mathlib.LinearAlgebra.Contraction
+import Mathlib.LinearAlgebra.Basis
+import Mathlib.LinearAlgebra.Contraction
 
 open BigOperators
 open Finset
 
+lemma OrthonormalBasis.sum_repr'
+  {𝕜 : Type*} [RCLike 𝕜]
+  {E : Type*} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
+  [Fintype ι]
+  (b : OrthonormalBasis ι 𝕜 E)
+  (v : E) :
+  v = ∑ i, ⟪b i, v⟫_𝕜 • (b i) := by
+  nth_rw 1 [← (b.sum_repr v)]
+  simp_rw [b.repr_apply_apply v]
 
 variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
 
@@ -18,20 +27,20 @@ noncomputable def realInnerAsElementOfDualTensorprod
   : TensorProduct ℝ E E →ₗ[ℝ] ℝ := TensorProduct.lift bilinFormOfRealInner
 
 
-instance
+instance 
   {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]  [FiniteDimensional ℝ E]
-  : NormedAddCommGroup (TensorProduct ℝ E E) where
-    norm := by
-
+  : NormedAddCommGroup (TensorProduct ℝ E E) where 
+    norm := by 
+      
       sorry
-    dist_self := by
-
+    dist_self := by 
+      
       sorry
 
   sorry
 
 /-
-instance
+instance 
   {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]  [FiniteDimensional ℝ E]
   : InnerProductSpace ℝ (TensorProduct ℝ E E) where
     smul := _

Nevanlinna/mathlibAddOn.lean

@@ -1,35 +0,0 @@
-import Mathlib.Analysis.Calculus.ContDiff.Basic
-import Mathlib.Analysis.Calculus.FDeriv.Add
-
-variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
-variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
-variable {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
-variable {G : Type*} [NormedAddCommGroup G] [NormedSpace 𝕜 G]
-variable {G' : Type*} [NormedAddCommGroup G'] [NormedSpace 𝕜 G']
-variable {f f₀ f₁ g : E → F}
-variable {f' f₀' f₁' g' : E →L[𝕜] F}
-variable (e : E →L[𝕜] F)
-variable {x : E}
-variable {s t : Set E}
-variable {L L₁ L₂ : Filter E}
-
-variable {R : Type*} [Semiring R] [Module R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F]
-
-
--- import Mathlib.Analysis.Calculus.FDeriv.Add
-
-@[fun_prop]
-theorem Differentiable.const_smul' (h : Differentiable 𝕜 f) (c : R) :
-    Differentiable 𝕜 (c • f) := by
-  have : c • f = fun x ↦ c • f x := rfl
-  rw [this]
-  exact Differentiable.const_smul h c
-
-
--- Mathlib.Analysis.Calculus.ContDiff.Basic
-
-theorem ContDiff.const_smul' {f : E → F} (c : R) (hf : ContDiff 𝕜 n f) :
-    ContDiff 𝕜 n (c • f) := by
-  have : c • f = fun x ↦ c • f x := rfl
-  rw [this]
-  exact ContDiff.const_smul c hf

Nevanlinna/partialDeriv.lean

@@ -38,18 +38,12 @@ theorem partialDeriv_eventuallyEq
   exact fun v => rfl
 
 
-theorem partialDeriv_smul₁
-  {f : E → F}
-  {a : 𝕜}
-  {v : E} :
-  partialDeriv 𝕜 (a • v) f = a • partialDeriv 𝕜 v f := by
+theorem partialDeriv_smul₁ {f : E → F} {a : 𝕜} {v : E} : partialDeriv 𝕜 (a • v) f = a • partialDeriv 𝕜 v f := by
   unfold partialDeriv
   conv =>
     left
     intro w
     rw [map_smul]
-  funext w
-  simp
 
 
 theorem partialDeriv_add₁ {f : E → F} {v₁ v₂ : E} : partialDeriv 𝕜 (v₁ + v₂) f = (partialDeriv 𝕜 v₁ f) + (partialDeriv 𝕜 v₂ f) := by
@@ -58,8 +52,6 @@ theorem partialDeriv_add₁ {f : E → F} {v₁ v₂ : E} : partialDeriv 𝕜 (v
     left
     intro w
     rw [map_add]
-  funext w
-  simp
 
 
 theorem partialDeriv_smul₂ {f : E → F} {a : 𝕜} {v : E} : partialDeriv 𝕜 v (a • f) = a • partialDeriv 𝕜 v f := by
@@ -78,7 +70,7 @@ theorem partialDeriv_smul₂ {f : E → F} {a : 𝕜} {v : E} : partialDeriv
         let ZZ := DifferentiableAt.const_smul contra a⁻¹
         have : (fun y => a⁻¹ • a • f y) = f := by
           funext i
-          rw [← smul_assoc, smul_eq_mul, mul_comm, mul_inv_cancel₀ ha]
+          rw [← smul_assoc, smul_eq_mul, mul_comm, mul_inv_cancel ha]
           simp
         rw [this] at ZZ
         exact hf ZZ
@@ -98,8 +90,6 @@ theorem partialDeriv_add₂ {f₁ f₂ : E → F} (h₁ : Differentiable 𝕜 f
     intro w
     left
     rw [fderiv_add (h₁ w) (h₂ w)]
-  funext w
-  simp
 
 
 theorem partialDeriv_add₂_differentiableAt
@@ -139,57 +129,6 @@ theorem partialDeriv_add₂_contDiffAt
     exact (hf₂' x (Set.mem_of_mem_inter_right hx)).differentiableAt
 
 
-theorem partialDeriv_sub₂ {f₁ f₂ : E → F} (h₁ : Differentiable 𝕜 f₁) (h₂ : Differentiable 𝕜 f₂) : ∀ v : E, partialDeriv 𝕜 v (f₁ - f₂) = (partialDeriv 𝕜 v f₁) - (partialDeriv 𝕜 v f₂) := by
-  unfold partialDeriv
-  intro v
-  have : f₁ - f₂ = fun y ↦ f₁ y - f₂ y := by rfl
-  rw [this]
-  conv =>
-    left
-    intro w
-    left
-    rw [fderiv_sub (h₁ w) (h₂ w)]
-  funext w
-  simp
-
-
-theorem partialDeriv_sub₂_differentiableAt
-  {f₁ f₂ : E → F}
-  {v : E}
-  {x : E}
-  (h₁ : DifferentiableAt 𝕜 f₁ x)
-  (h₂ : DifferentiableAt 𝕜 f₂ x) :
-  partialDeriv 𝕜 v (f₁ - f₂) x = (partialDeriv 𝕜 v f₁) x - (partialDeriv 𝕜 v f₂) x := by
-
-  unfold partialDeriv
-  have : f₁ - f₂ = fun y ↦ f₁ y - f₂ y := by rfl
-  rw [this]
-  rw [fderiv_sub h₁ h₂]
-  rfl
-
-
-theorem partialDeriv_sub₂_contDiffAt
-  {f₁ f₂ : E → F}
-  {v : E}
-  {x : E}
-  (h₁ : ContDiffAt 𝕜 1 f₁ x)
-  (h₂ : ContDiffAt 𝕜 1 f₂ x) :
-  partialDeriv 𝕜 v (f₁ - f₂) =ᶠ[nhds x] (partialDeriv 𝕜 v f₁) - (partialDeriv 𝕜 v f₂) := by
-
-  obtain ⟨f₁', u₁, hu₁, _, hf₁'⟩ := contDiffAt_one_iff.1 h₁
-  obtain ⟨f₂', u₂, hu₂, _, hf₂'⟩ := contDiffAt_one_iff.1 h₂
-
-  apply Filter.eventuallyEq_iff_exists_mem.2
-  use u₁ ∩ u₂
-  constructor
-  · exact Filter.inter_mem hu₁ hu₂
-  · intro x hx
-    simp
-    apply partialDeriv_sub₂_differentiableAt 𝕜
-    exact (hf₁' x (Set.mem_of_mem_inter_left hx)).differentiableAt
-    exact (hf₂' x (Set.mem_of_mem_inter_right hx)).differentiableAt
-
-
 theorem partialDeriv_compContLin
   {f : E → F}
   {l : F →L[𝕜] G}
@@ -297,7 +236,7 @@ lemma partialDeriv_fderivOn
   rw [fderiv_clm_apply]
   · simp
   · convert DifferentiableOn.differentiableAt _ (IsOpen.mem_nhds hs hz)
-    apply ContDiffOn.differentiableOn _ (Preorder.le_refl 1)
+    apply ContDiffOn.differentiableOn _ (Submonoid.oneLE.proof_2 ℕ∞)
     exact ((contDiffOn_succ_iff_fderiv_of_isOpen hs).1 hf).2
   · simp
 
@@ -356,11 +295,11 @@ theorem partialDeriv_smul'₂
       left_inv := by
         intro x
         simp
-        rw [← smul_assoc, smul_eq_mul, mul_comm, mul_inv_cancel₀ ha, one_smul]
+        rw [← smul_assoc, smul_eq_mul, mul_comm, mul_inv_cancel ha, one_smul]
       right_inv := by
         intro x
         simp
-        rw [← smul_assoc, smul_eq_mul, mul_inv_cancel₀ ha, one_smul]
+        rw [← smul_assoc, smul_eq_mul, mul_inv_cancel ha, one_smul]
       continuous_toFun := continuous_const_smul a
       continuous_invFun := continuous_const_smul a⁻¹
     }
@@ -407,7 +346,7 @@ theorem partialDeriv_comm
     let f'' := (fderiv ℝ f' z)
     have h₁ : HasFDerivAt f' f'' z := by
       apply DifferentiableAt.hasFDerivAt
-      apply (contDiff_succ_iff_fderiv.1 h).right.differentiable (Preorder.le_refl 1)
+      apply (contDiff_succ_iff_fderiv.1 h).right.differentiable (Submonoid.oneLE.proof_2 ℕ∞)
 
     apply second_derivative_symmetric h₀ h₁ v₁ v₂
 
@@ -441,7 +380,7 @@ theorem partialDeriv_commOn
     have h₁ : HasFDerivAt f' f'' z := by
       apply DifferentiableAt.hasFDerivAt
       apply DifferentiableOn.differentiableAt _ (IsOpen.mem_nhds hs hz)
-      apply ContDiffOn.differentiableOn _ (Preorder.le_refl 1)
+      apply ContDiffOn.differentiableOn _ (Submonoid.oneLE.proof_2 ℕ∞)
       exact ((contDiffOn_succ_iff_fderiv_of_isOpen hs).1 h).2
 
     have h₀' : ∀ᶠ (y : E) in nhds z, HasFDerivAt f (f' y) y := by

Nevanlinna/periodic_integrability.lean

@@ -1,101 +0,0 @@
-import Mathlib.MeasureTheory.Integral.Periodic
-
-
-theorem periodic_integrability₁
-  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E]
-  {f : ℝ → E}
-  {t T : ℝ}
-  {n : ℕ}
-  (h₁f : Function.Periodic f T)
-  (h₂f : IntervalIntegrable f MeasureTheory.volume t (t + T)) :
-  IntervalIntegrable f MeasureTheory.volume t (t + n * T) := by
-  induction' n with n hn
-  simp
-  apply IntervalIntegrable.trans (b := t + n * T)
-  exact hn
-
-  let A := IntervalIntegrable.comp_sub_right h₂f (n * T)
-  have : f = fun x ↦ f (x - n * T) := by simp [Function.Periodic.sub_nat_mul_eq h₁f n]
-  simp_rw [← this] at A
-  have : (t + T + ↑n * T) = (t + ↑(n + 1) * T) := by simp; ring
-  simp_rw [this] at A
-  exact A
-
-theorem periodic_integrability₂
-  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E]
-  {f : ℝ → E}
-  {t T : ℝ}
-  {n : ℕ}
-  (h₁f : Function.Periodic f T)
-  (h₂f : IntervalIntegrable f MeasureTheory.volume t (t + T)) :
-  IntervalIntegrable f MeasureTheory.volume (t - n * T) t := by
-  induction' n with n hn
-  simp
-  --
-  apply IntervalIntegrable.trans (b := t - n * T)
-  --
-  have A := IntervalIntegrable.comp_add_right h₂f (((n + 1): ℕ) * T)
-
-  have : f = fun x ↦ f (x + ((n + 1) : ℕ) * T) := by
-    funext x
-    have : x = x + ↑(n + 1) * T - ↑(n + 1) * T := by ring
-    nth_rw 1 [this]
-    rw [Function.Periodic.sub_nat_mul_eq h₁f]
-  simp_rw [← this] at A
-  have : (t + T - ↑(n + 1) * T) = (t - ↑n * T) := by simp; ring
-  simp_rw [this] at A
-  exact A
-  --
-  exact hn
-
-
-theorem periodic_integrability₃
-  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E]
-  {f : ℝ → E}
-  {t T : ℝ}
-  {n₁ n₂ : ℕ}
-  (h₁f : Function.Periodic f T)
-  (h₂f : IntervalIntegrable f MeasureTheory.volume t (t + T)) :
-  IntervalIntegrable f MeasureTheory.volume (t - n₁ * T) (t + n₂ * T) := by
-  apply IntervalIntegrable.trans (b := t)
-  exact periodic_integrability₂ h₁f h₂f
-  exact periodic_integrability₁ h₁f h₂f
-
-
-theorem periodic_integrability4
-  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E]
-  {f : ℝ → E}
-  {t T : ℝ}
-  {a₁ a₂ : ℝ}
-  (h₁f : Function.Periodic f T)
-  (hT : 0 < T)
-  (h₂f : IntervalIntegrable f MeasureTheory.volume t (t + T)) :
-  IntervalIntegrable f MeasureTheory.volume a₁ a₂ := by
-
-  obtain ⟨n₁, hn₁⟩ : ∃ n₁ : ℕ, t - n₁ * T ≤ min a₁ a₂ := by
-    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 [sub_le_iff_le_add] at hn₁
-    rw [add_comm]
-    exact hn₁
-  obtain ⟨n₂, hn₂⟩ : ∃ n₂ : ℕ, max a₁ a₂ ≤ t + n₂ * T := by
-    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₂
-    linarith
-
-  have : Set.uIcc a₁ a₂ ⊆ Set.uIcc (t - n₁ * T) (t + n₂ * T) := by
-    apply Set.uIcc_subset_uIcc_iff_le.mpr
-    constructor
-    · calc min (t - ↑n₁ * T) (t + ↑n₂ * T)
-      _ ≤ (t - ↑n₁ * T) := by exact min_le_left (t - ↑n₁ * T) (t + ↑n₂ * T)
-      _ ≤ min a₁ a₂ := by exact hn₁
-    · calc max a₁ a₂
-      _ ≤ t + n₂ * T := by exact hn₂
-      _ ≤ max (t - ↑n₁ * T) (t + ↑n₂ * T) := by exact le_max_right (t - ↑n₁ * T) (t + ↑n₂ * T)
-
-  apply IntervalIntegrable.mono_set _ this
-  exact periodic_integrability₃ h₁f h₂f

Nevanlinna/smulImprovement.lean

@@ -0,0 +1,40 @@
+import Mathlib.Analysis.Complex.CauchyIntegral
+--import Mathlib.Analysis.Complex.Module
+
+
+
+example simplificationTest₁
+  {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] [IsScalarTower ℝ ℂ E]
+  {v : E}
+  {z : ℂ} :
+  z • v =  z.re • v + Complex.I • z.im • v := by
+
+  /-
+  An attempt to write  "rw [add_smul]" will fail with "did not find instance of
+  the pattern in the target -- expression (?r + ?s) • ?x".
+  -/
+  sorry
+
+
+theorem add_smul'
+  (𝕜₁ : Type*) [NontriviallyNormedField ℝ]
+  {𝕜₂ : Type*} [NontriviallyNormedField ℂ] [NormedAlgebra ℝ ℂ]
+  {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] [IsScalarTower ℝ ℂ E]
+  {v : E}
+  {r s : ℂ} :
+  (r + s) • v = r • v + s • v :=
+  Module.add_smul r s v
+
+
+theorem smul_add' (a : M) (b₁ b₂ : A) : a • (b₁ + b₂) = a • b₁ + a • b₂ :=
+  DistribSMul.smul_add _ _ _
+#align smul_add smul_add
+
+
+
+
+example simplificationTest₂
+  {v : E}
+  {z : ℂ} :
+  z • v =  z.re • v + Complex.I • z.im • v := by
+  sorry

Nevanlinna/specialFunctions_CircleIntegral_affine.lean

@@ -1,384 +0,0 @@
-import Mathlib.MeasureTheory.Integral.Periodic
-import Mathlib.MeasureTheory.Integral.CircleIntegral
-import Nevanlinna.specialFunctions_Integral_log_sin
-import Nevanlinna.harmonicAt_examples
-import Nevanlinna.harmonicAt_meanValue
-import Nevanlinna.periodic_integrability
-
-open scoped Interval Topology
-open Real Filter MeasureTheory intervalIntegral
-
-
-
--- Lemmas for the circleMap
-
-lemma l₀ {x₁ x₂ : ℝ} : (circleMap 0 1 x₁) * (circleMap 0 1 x₂) = circleMap 0 1 (x₁+x₂) := by
-  dsimp [circleMap]
-  simp
-  rw [add_mul, Complex.exp_add]
-
-lemma l₁ {x : ℝ} : ‖circleMap 0 1 x‖ = 1 := by
-  rw [Complex.norm_eq_abs, abs_circleMap_zero]
-  simp
-
-lemma l₂ {x : ℝ} : ‖(circleMap 0 1 x) - a‖ = ‖1 - (circleMap 0 1 (-x)) * a‖ := by
-  calc ‖(circleMap 0 1 x) - a‖
-  _ = 1 * ‖(circleMap 0 1 x) - a‖ := by
-    exact Eq.symm (one_mul ‖circleMap 0 1 x - a‖)
-  _ = ‖(circleMap 0 1 (-x))‖ * ‖(circleMap 0 1 x) - a‖ := by
-    rw [l₁]
-  _ = ‖(circleMap 0 1 (-x)) * ((circleMap 0 1 x) - a)‖ := by
-    exact Eq.symm (NormedField.norm_mul' (circleMap 0 1 (-x)) (circleMap 0 1 x - a))
-  _ = ‖(circleMap 0 1 (-x)) * (circleMap 0 1 x) - (circleMap 0 1 (-x)) * a‖ := by
-    rw [mul_sub]
-  _ = ‖(circleMap 0 1 0) - (circleMap 0 1 (-x)) * a‖ := by
-    rw [l₀]
-    simp
-  _ = ‖1 - (circleMap 0 1 (-x)) * a‖ := by
-    congr
-    dsimp [circleMap]
-    simp
-
-
--- Integral of log ‖circleMap 0 1 x - a‖, for ‖a‖ < 1.
-
-lemma int'₀
-  {a : ℂ}
-  (ha : a ∈ Metric.ball 0 1) :
-  IntervalIntegrable (fun x ↦ log ‖circleMap 0 1 x - a‖) volume 0 (2 * π) := by
-  apply Continuous.intervalIntegrable
-  apply Continuous.log
-  fun_prop
-  simp
-  intro x
-  by_contra h₁a
-  rw [← h₁a] at ha
-  simp at ha
-
-
-lemma int₀
-  {a : ℂ}
-  (ha : a ∈ Metric.ball 0 1) :
-  ∫ (x : ℝ) in (0)..2 * π, log ‖circleMap 0 1 x - a‖ = 0 := by
-
-  by_cases h₁a : a = 0
-  · -- case: a = 0
-    rw [h₁a]
-    simp
-
-  -- case: a ≠ 0
-  simp_rw [l₂]
-  have {x : ℝ} : log ‖1 - circleMap 0 1 (-x) * a‖ = (fun w ↦ log ‖1 - circleMap 0 1 (w) * a‖) (-x) := by rfl
-  conv =>
-    left
-    arg 1
-    intro x
-    rw [this]
-  rw [intervalIntegral.integral_comp_neg ((fun w ↦ log ‖1 - circleMap 0 1 (w) * a‖))]
-
-  let f₁ := fun w ↦ log ‖1 - circleMap 0 1 w * a‖
-  have {x : ℝ} : log ‖1 - circleMap 0 1 x * a‖ = f₁ (x + 2 * π) := by
-    dsimp [f₁]
-    congr 4
-    let A := periodic_circleMap 0 1 x
-    simp at A
-    exact id (Eq.symm A)
-  conv =>
-    left
-    arg 1
-    intro x
-    rw [this]
-  rw [intervalIntegral.integral_comp_add_right f₁ (2 * π)]
-  simp
-  dsimp [f₁]
-
-  let ρ := ‖a‖⁻¹
-  have hρ : 1 < ρ := by
-    apply one_lt_inv_iff.mpr
-    constructor
-    · exact norm_pos_iff'.mpr h₁a
-    · exact mem_ball_zero_iff.mp ha
-
-  let F := fun z ↦ log ‖1 - z * a‖
-
-  have hf : ∀ x ∈ Metric.ball 0 ρ, HarmonicAt F x := by
-    intro x hx
-    apply logabs_of_holomorphicAt_is_harmonic
-    apply Differentiable.holomorphicAt
-    fun_prop
-    apply sub_ne_zero_of_ne
-    by_contra h
-    have : ‖x * a‖ < 1 := by
-      calc ‖x * a‖
-      _ = ‖x‖ * ‖a‖ := by exact NormedField.norm_mul' x a
-      _ < ρ * ‖a‖ := by
-        apply (mul_lt_mul_right _).2
-        exact mem_ball_zero_iff.mp hx
-        exact norm_pos_iff'.mpr h₁a
-      _ = 1 := by
-        dsimp [ρ]
-        apply inv_mul_cancel₀
-        exact (AbsoluteValue.ne_zero_iff Complex.abs).mpr h₁a
-    rw [← h] at this
-    simp at this
-
-  let A := harmonic_meanValue ρ 1 zero_lt_one hρ hf
-  dsimp [F] at A
-  simp at A
-  exact A
-
-
--- Integral of log ‖circleMap 0 1 x - 1‖
-
-lemma int₁₁ : ∫ (x : ℝ) in (0)..π, log (4 * sin x ^ 2) = 0 := by
-
-  have t₁ {x : ℝ} : x ∈ Set.Ioo 0 π → log (4 * sin x ^ 2) = log 4 + 2 * log (sin x) := by
-    intro hx
-    rw [log_mul, log_pow]
-    rfl
-    exact Ne.symm (NeZero.ne' 4)
-    apply pow_ne_zero 2
-    apply (fun a => Ne.symm (ne_of_lt a))
-    exact sin_pos_of_mem_Ioo hx
-
-
-  have t₂ : Set.EqOn (fun y ↦ log (4 * sin y ^ 2)) (fun y ↦ log 4 + 2 * log (sin y)) (Set.Ioo 0 π) := by
-    intro x hx
-    simp
-    rw [t₁ hx]
-
-  rw [intervalIntegral.integral_congr_volume pi_pos t₂]
-  rw [intervalIntegral.integral_add]
-  rw [intervalIntegral.integral_const_mul]
-  simp
-  rw [integral_log_sin₂]
-  have : (4 : ℝ) = 2 * 2 := by norm_num
-  rw [this, log_mul]
-  ring
-  norm_num
-  norm_num
-  -- IntervalIntegrable (fun x => log 4) volume 0 π
-  simp
-  -- IntervalIntegrable (fun x => 2 * log (sin x)) volume 0 π
-  apply IntervalIntegrable.const_mul
-  exact intervalIntegrable_log_sin
-
-lemma logAffineHelper {x : ℝ} : log ‖circleMap 0 1 x - 1‖ = log (4 * sin (x / 2) ^ 2) / 2 := by
-  dsimp [Complex.abs]
-  rw [log_sqrt (Complex.normSq_nonneg (circleMap 0 1 x - 1))]
-  congr
-  calc Complex.normSq (circleMap 0 1 x - 1)
-  _ = (cos x - 1) * (cos x - 1) + sin x * sin x := by
-    dsimp [circleMap]
-    rw [Complex.normSq_apply]
-    simp
-  _ = sin x ^ 2 + cos x ^ 2 + 1 - 2 * cos x := by
-    ring
-  _ = 2 - 2 * cos x := by
-    rw [sin_sq_add_cos_sq]
-    norm_num
-  _ = 2 - 2 * cos (2 * (x / 2)) := by
-    rw [← mul_div_assoc]
-    congr; norm_num
-  _ = 4 - 4 * cos (x / 2) ^ 2 := by
-    rw [cos_two_mul]
-    ring
-  _ = 4 * sin (x / 2) ^ 2 := by
-    nth_rw 1 [← mul_one 4, ← sin_sq_add_cos_sq (x / 2)]
-    ring
-
-lemma int'₁ : -- Integrability of log ‖circleMap 0 1 x - 1‖
-  IntervalIntegrable (fun x ↦ log ‖circleMap 0 1 x - 1‖) volume 0 (2 * π) := by
-
-  simp_rw [logAffineHelper]
-  apply IntervalIntegrable.div_const
-  rw [← IntervalIntegrable.comp_mul_left_iff (c := 2) (Ne.symm (NeZero.ne' 2))]
-  simp
-
-  have h₁ : Set.EqOn (fun x => log (4 * sin x ^ 2)) (fun x => log 4 + 2 * log (sin x)) (Set.Ioo 0 π) := by
-    intro x hx
-    simp [log_mul (Ne.symm (NeZero.ne' 4)), log_pow, ne_of_gt (sin_pos_of_mem_Ioo hx)]
-  rw [IntervalIntegrable.integral_congr_Ioo pi_nonneg h₁]
-  apply IntervalIntegrable.add
-  simp
-  apply IntervalIntegrable.const_mul
-  exact intervalIntegrable_log_sin
-
-lemma int''₁ : -- Integrability of log ‖circleMap 0 1 x - 1‖ for arbitrary intervals
-  ∀ (t₁ t₂ : ℝ), IntervalIntegrable (fun x ↦ log ‖circleMap 0 1 x - 1‖) volume t₁ t₂ := by
-  intro t₁ t₂
-
-  apply periodic_integrability4 (T := 2 * π) (t := 0)
-  --
-  have : (fun x => log ‖circleMap 0 1 x - 1‖) = (fun x => log ‖x - 1‖) ∘ (circleMap 0 1) := rfl
-  rw [this]
-  apply Function.Periodic.comp
-  exact periodic_circleMap 0 1
-  --
-  exact two_pi_pos
-  --
-  rw [zero_add]
-  exact int'₁
-
-lemma int₁ :
-  ∫ x in (0)..(2 * π), log ‖circleMap 0 1 x - 1‖ = 0 := by
-
-  simp_rw [logAffineHelper]
-  simp
-
-  have : ∫ (x : ℝ) in (0)..2 * π, log (4 * sin (x / 2) ^ 2) =  2 * ∫ (x : ℝ) in (0)..π, log (4 * sin x ^ 2) := by
-    have : 1 = 2 * (2 : ℝ)⁻¹ := by exact Eq.symm (mul_inv_cancel_of_invertible 2)
-    nth_rw 1 [← one_mul (∫ (x : ℝ) in (0)..2 * π, log (4 * sin (x / 2) ^ 2))]
-    rw [← mul_inv_cancel_of_invertible 2, mul_assoc]
-    let f := fun y ↦ log (4 * sin y ^ 2)
-    have {x : ℝ} : log (4 * sin (x / 2) ^ 2) = f (x / 2) := by simp
-    conv =>
-      left
-      right
-      right
-      arg 1
-      intro x
-      rw [this]
-    rw [intervalIntegral.inv_mul_integral_comp_div 2]
-    simp
-  rw [this]
-  simp
-  exact int₁₁
-
-
--- Integral of log ‖circleMap 0 1 x - a‖, for ‖a‖ = 1
-
-lemma int'₂
-  {a : ℂ}
-  (ha : ‖a‖ = 1) :
-  IntervalIntegrable (fun x ↦ log ‖circleMap 0 1 x - a‖) volume 0 (2 * π) := by
-
-  simp_rw [l₂]
-  have {x : ℝ} : log ‖1 - circleMap 0 1 (-x) * a‖ = (fun w ↦ log ‖1 - circleMap 0 1 (w) * a‖) (-x) := by rfl
-  conv =>
-    arg 1
-    intro x
-    rw [this]
-  rw [IntervalIntegrable.iff_comp_neg]
-
-  let f₁ := fun w ↦ log ‖1 - circleMap 0 1 w * a‖
-  have {x : ℝ} : log ‖1 - circleMap 0 1 x * a‖ = f₁ (x + 2 * π) := by
-    dsimp [f₁]
-    congr 4
-    let A := periodic_circleMap 0 1 x
-    simp at A
-    exact id (Eq.symm A)
-  conv =>
-    arg 1
-    intro x
-    arg 0
-    intro w
-    rw [this]
-  simp
-  have : 0 = 2 * π - 2 * π := by ring
-  rw [this]
-  have : -(2 * π ) = 0 - 2 * π := by ring
-  rw [this]
-  apply IntervalIntegrable.comp_add_right _ (2 * π) --f₁ (2 * π)
-  dsimp [f₁]
-
-  have : ∃ ζ, a = circleMap 0 1 ζ := by
-    apply Set.exists_range_iff.mp
-    use a
-    simp
-    exact ha
-  obtain ⟨ζ, hζ⟩ := this
-  rw [hζ]
-  simp_rw [l₀]
-
-  have : 2 * π  = (2 * π + ζ) - ζ := by ring
-  rw [this]
-  have : 0 = ζ - ζ := by ring
-  rw [this]
-  have : (fun w => log (Complex.abs (1 - circleMap 0 1 (w + ζ)))) = fun x ↦ (fun w ↦ log (Complex.abs (1 - circleMap 0 1 (w)))) (x + ζ) := rfl
-  rw [this]
-  apply IntervalIntegrable.comp_add_right (f := (fun w ↦ log (Complex.abs (1 - circleMap 0 1 (w))))) _ ζ
-
-  have : Function.Periodic (fun x ↦ log (Complex.abs (1 - circleMap 0 1 x))) (2 * π) := by
-    have : (fun x ↦ log (Complex.abs (1 - circleMap 0 1 x))) = ( (fun x ↦ log (Complex.abs (1 - x))) ∘ (circleMap 0 1) ) := by rfl
-    rw [this]
-    apply Function.Periodic.comp
-    exact periodic_circleMap 0 1
-
-  let A := int''₁ (2 * π + ζ) ζ
-  have {x : ℝ} : ‖circleMap 0 1 x - 1‖ = Complex.abs (1 - circleMap 0 1 x) := AbsoluteValue.map_sub Complex.abs (circleMap 0 1 x) 1
-  simp_rw [this] at A
-  exact A
-
-
-lemma int₂
-  {a : ℂ}
-  (ha : ‖a‖ = 1) :
-  ∫ x in (0)..(2 * π), log ‖circleMap 0 1 x - a‖ = 0 := by
-
-  simp_rw [l₂]
-  have {x : ℝ} : log ‖1 - circleMap 0 1 (-x) * a‖ = (fun w ↦ log ‖1 - circleMap 0 1 (w) * a‖) (-x) := by rfl
-  conv =>
-    left
-    arg 1
-    intro x
-    rw [this]
-  rw [intervalIntegral.integral_comp_neg ((fun w ↦ log ‖1 - circleMap 0 1 (w) * a‖))]
-
-  let f₁ := fun w ↦ log ‖1 - circleMap 0 1 w * a‖
-  have {x : ℝ} : log ‖1 - circleMap 0 1 x * a‖ = f₁ (x + 2 * π) := by
-    dsimp [f₁]
-    congr 4
-    let A := periodic_circleMap 0 1 x
-    simp at A
-    exact id (Eq.symm A)
-  conv =>
-    left
-    arg 1
-    intro x
-    rw [this]
-  rw [intervalIntegral.integral_comp_add_right f₁ (2 * π)]
-  simp
-  dsimp [f₁]
-
-  have : ∃ ζ, a = circleMap 0 1 ζ := by
-    apply Set.exists_range_iff.mp
-    use a
-    simp
-    exact ha
-  obtain ⟨ζ, hζ⟩ := this
-  rw [hζ]
-  simp_rw [l₀]
-
-  rw [intervalIntegral.integral_comp_add_right (f := fun x ↦ log (Complex.abs (1 - circleMap 0 1 (x))))]
-
-  have : Function.Periodic (fun x ↦ log (Complex.abs (1 - circleMap 0 1 x))) (2 * π) := by
-    have : (fun x ↦ log (Complex.abs (1 - circleMap 0 1 x))) = ( (fun x ↦ log (Complex.abs (1 - x))) ∘ (circleMap 0 1) ) := by rfl
-    rw [this]
-    apply Function.Periodic.comp
-    exact periodic_circleMap 0 1
-
-  let A := Function.Periodic.intervalIntegral_add_eq this ζ 0
-  simp at A
-  simp
-  rw [add_comm]
-  rw [A]
-
-  have {x : ℝ} : log (Complex.abs (1 - circleMap 0 1 x)) = log ‖circleMap 0 1 x - 1‖ := by
-    rw [← AbsoluteValue.map_neg Complex.abs]
-    simp
-  simp_rw [this]
-  exact int₁
-
-
-lemma int₃
-  {a : ℂ}
-  (ha : a ∈ Metric.closedBall 0 1) :
-  ∫ x in (0)..(2 * π), log ‖circleMap 0 1 x - a‖ = 0 := by
-  by_cases h₁a : a ∈ Metric.ball 0 1
-  · exact int₀ h₁a
-  · apply int₂
-    simp at ha
-    simp at h₁a
-    simp
-    linarith

Nevanlinna/specialFunctions_Integral_log.lean

@@ -1,65 +0,0 @@
-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]

Nevanlinna/specialFunctions_Integral_log_sin.lean

@@ -1,374 +0,0 @@
-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
-
-
-
-lemma logsinBound : ∀ x ∈ (Set.Icc 0 1), ‖(log ∘ sin) x‖ ≤ ‖log ((π / 2)⁻¹ * x)‖ := by
-
-  intro x hx
-  by_cases h'x : x = 0
-  · rw [h'x]; simp
-
-  -- Now handle the case where x ≠ 0
-  have l₀ : log ((π / 2)⁻¹ * x) ≤ 0 := by
-    apply log_nonpos
-    apply mul_nonneg
-    apply le_of_lt
-    apply inv_pos.2
-    apply div_pos
-    exact pi_pos
-    exact zero_lt_two
-    apply (Set.mem_Icc.1 hx).1
-    simp
-    apply mul_le_one
-    rw [div_le_one pi_pos]
-    exact two_le_pi
-    exact (Set.mem_Icc.1 hx).1
-    exact (Set.mem_Icc.1 hx).2
-
-  have l₁ : 0 ≤ sin x := by
-    apply sin_nonneg_of_nonneg_of_le_pi (Set.mem_Icc.1 hx).1
-    trans (1 : ℝ)
-    exact (Set.mem_Icc.1 hx).2
-    trans π / 2
-    exact one_le_pi_div_two
-    norm_num [pi_nonneg]
-  have l₂ : log (sin x) ≤ 0 := log_nonpos l₁ (sin_le_one x)
-
-  simp only [norm_eq_abs, Function.comp_apply]
-  rw [abs_eq_neg_self.2 l₀]
-  rw [abs_eq_neg_self.2 l₂]
-  simp only [neg_le_neg_iff, ge_iff_le]
-
-  have l₃ : x ∈ (Set.Ioi 0) := by
-    simp
-    exact lt_of_le_of_ne (Set.mem_Icc.1 hx).1 ( fun a => h'x (id (Eq.symm a)) )
-
-  have l₅ : 0 < (π / 2)⁻¹ * x := by
-    apply mul_pos
-    apply inv_pos.2
-    apply div_pos pi_pos zero_lt_two
-    exact l₃
-
-  have : ∀ x ∈ (Set.Icc 0 (π / 2)), (π / 2)⁻¹ * x ≤ sin x := by
-    intro x hx
-
-    have i₀ : 0 ∈ Set.Icc 0 π :=
-      Set.left_mem_Icc.mpr pi_nonneg
-    have i₁ : π / 2 ∈ Set.Icc 0 π :=
-      Set.mem_Icc.mpr ⟨div_nonneg pi_nonneg zero_le_two, half_le_self pi_nonneg⟩
-
-    have i₂ : 0 ≤ 1 - (π / 2)⁻¹ * x := by
-      rw [sub_nonneg]
-      calc (π / 2)⁻¹ * x
-      _ ≤ (π / 2)⁻¹ * (π / 2) := by
-        apply mul_le_mul_of_nonneg_left
-        exact (Set.mem_Icc.1 hx).2
-        apply inv_nonneg.mpr (div_nonneg pi_nonneg zero_le_two)
-      _ = 1 := by
-        apply inv_mul_cancel₀
-        apply div_ne_zero_iff.mpr
-        constructor
-        · exact pi_ne_zero
-        · exact Ne.symm (NeZero.ne' 2)
-
-    have i₃ : 0 ≤ (π / 2)⁻¹ * x := by
-      apply mul_nonneg
-      apply inv_nonneg.2
-      apply div_nonneg
-      exact pi_nonneg
-      exact zero_le_two
-      exact (Set.mem_Icc.1 hx).1
-
-    have i₄ : 1 - (π / 2)⁻¹ * x + (π / 2)⁻¹ * x = 1 := by ring
-
-    let B := strictConcaveOn_sin_Icc.concaveOn.2 i₀ i₁ i₂ i₃ i₄
-    simp [Real.sin_pi_div_two] at B
-    rw [(by ring_nf; rw [mul_inv_cancel₀ pi_ne_zero, one_mul] : 2 / π * x * (π / 2) = x)] at B
-    simpa
-
-  apply log_le_log l₅
-  apply this
-  apply Set.mem_Icc.mpr
-  constructor
-  · exact le_of_lt l₃
-  · trans 1
-    exact (Set.mem_Icc.1 hx).2
-    exact one_le_pi_div_two
-
-
-lemma intervalIntegrable_log_sin₁ : IntervalIntegrable (log ∘ sin) volume 0 1 := by
-
-  have int_log : IntervalIntegrable (fun x ↦ ‖log x‖) volume 0 1 := by
-    apply IntervalIntegrable.norm
-    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 int_log : IntervalIntegrable (fun x ↦ ‖log ((π / 2)⁻¹ * x)‖) volume 0 1 := by
-
-    have A := IntervalIntegrable.comp_mul_right int_log (π / 2)⁻¹
-    simp only [norm_eq_abs] at A
-    conv =>
-      arg 1
-      intro x
-      rw [mul_comm]
-    simp only [norm_eq_abs]
-    apply IntervalIntegrable.mono A
-    simp
-    trans Set.Icc 0 (π / 2)
-    exact Set.Icc_subset_Icc (Preorder.le_refl 0) one_le_pi_div_two
-    exact Set.Icc_subset_uIcc
-    exact Preorder.le_refl volume
-
-  apply IntervalIntegrable.mono_fun' (g := fun x ↦ ‖log ((π / 2)⁻¹ * x)‖)
-  exact int_log
-
-  -- AEStronglyMeasurable (log ∘ sin) (volume.restrict (Ι 0 1))
-  apply ContinuousOn.aestronglyMeasurable
-  apply ContinuousOn.comp (t := Ι 0 1)
-  apply ContinuousOn.mono (s := {0}ᶜ)
-  exact continuousOn_log
-  intro x hx
-  by_contra contra
-  simp at contra
-  rw [contra, Set.left_mem_uIoc] at hx
-  linarith
-  exact continuousOn_sin
-
-  -- Set.MapsTo sin (Ι 0 1) (Ι 0 1)
-  rw [Set.uIoc_of_le (zero_le_one' ℝ)]
-  exact fun x hx ↦ ⟨sin_pos_of_pos_of_le_one hx.1 hx.2, sin_le_one x⟩
-
-  -- MeasurableSet (Ι 0 1)
-  exact measurableSet_uIoc
-
-  -- (fun x => ‖(log ∘ sin) x‖) ≤ᶠ[ae (volume.restrict (Ι 0 1))] ‖log‖
-  dsimp [EventuallyLE]
-  rw [MeasureTheory.ae_restrict_iff]
-  apply MeasureTheory.ae_of_all
-  intro x hx
-  have : x ∈ Set.Icc 0 1 := by
-    simp
-    simp at hx
-    constructor
-    · exact le_of_lt hx.1
-    · exact hx.2
-  let A := logsinBound x this
-  simp only [Function.comp_apply, norm_eq_abs] at A
-  exact A
-
-  apply measurableSet_le
-  apply Measurable.comp'
-  exact continuous_abs.measurable
-  exact Measurable.comp' measurable_log continuous_sin.measurable
-  -- Measurable fun a => |log ((π / 2)⁻¹ * a)|
-  apply Measurable.comp'
-  exact continuous_abs.measurable
-  apply Measurable.comp'
-  exact measurable_log
-  exact measurable_const_mul (π / 2)⁻¹
-
-lemma intervalIntegrable_log_sin₂ : IntervalIntegrable (log ∘ sin) volume 0 (π / 2) := by
-
-  apply IntervalIntegrable.trans (b := 1)
-  exact intervalIntegrable_log_sin₁
-
-  -- IntervalIntegrable (log ∘ sin) volume 1 (π / 2)
-  apply ContinuousOn.intervalIntegrable
-  apply ContinuousOn.comp continuousOn_log continuousOn_sin
-  intro x hx
-  rw [Set.uIcc_of_le, Set.mem_Icc] at hx
-  have : 0 < sin x := by
-    apply Real.sin_pos_of_pos_of_lt_pi
-    · calc 0
-      _ < 1 := Real.zero_lt_one
-      _ ≤ x := hx.1
-    · calc x
-      _ ≤ π / 2 := hx.2
-      _ < π := div_two_lt_of_pos pi_pos
-  by_contra h₁x
-  simp at h₁x
-  rw [h₁x] at this
-  simp at this
-  exact one_le_pi_div_two
-
-theorem intervalIntegrable_log_sin : IntervalIntegrable (log ∘ sin) volume 0 π := by
-  apply IntervalIntegrable.trans (b := π / 2)
-  exact intervalIntegrable_log_sin₂
-  -- IntervalIntegrable (log ∘ sin) volume (π / 2) π
-  let A := IntervalIntegrable.comp_sub_left intervalIntegrable_log_sin₂ π
-  simp at A
-  let B := IntervalIntegrable.symm A
-  have : π - π / 2 = π / 2 := by linarith
-  rwa [this] at B
-
-theorem intervalIntegrable_log_cos : IntervalIntegrable (log ∘ cos) volume 0 (π / 2) := by
-  let A := IntervalIntegrable.comp_sub_left intervalIntegrable_log_sin₂ (π / 2)
-  simp only [Function.comp_apply, sub_zero, sub_self] at A
-  simp_rw [sin_pi_div_two_sub] at A
-  have : (fun x => log (cos x)) = log ∘ cos := rfl
-  apply IntervalIntegrable.symm
-  rwa [← this]
-
-
-theorem intervalIntegral.integral_congr_volume
-  {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E]
-  {f : ℝ → E}
-  {g : ℝ → E}
-  {a : ℝ}
-  {b : ℝ}
-  (h₀ : a < b)
-  (h₁ : Set.EqOn f g (Set.Ioo a b)) :
-  ∫ (x : ℝ) in a..b, f x = ∫ (x : ℝ) in a..b, g x := by
-
-  apply intervalIntegral.integral_congr_ae
-  rw [MeasureTheory.ae_iff]
-  apply nonpos_iff_eq_zero.1
-  push_neg
-  have : {x | x ∈ Ι a b ∧ f x ≠ g x} ⊆ {b} := by
-    intro x hx
-    have t₂ : x ∈ Ι a b \ Set.Ioo a b := by
-      constructor
-      · exact hx.1
-      · by_contra H
-        exact hx.2 (h₁ H)
-    rw [Set.uIoc_of_le (le_of_lt h₀)] at t₂
-    rw [Set.Ioc_diff_Ioo_same h₀] at t₂
-    assumption
-  calc volume {a_1 | a_1 ∈ Ι a b ∧ f a_1 ≠ g a_1}
-  _ ≤ volume {b} := volume.mono this
-  _ = 0 := volume_singleton
-
-
-theorem IntervalIntegrable.integral_congr_Ioo
-  {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E]
-  {f g : ℝ → E}
-  {a b : ℝ}
-  (hab : a ≤ b)
-  (hfg : Set.EqOn f g (Set.Ioo a b)) :
-  IntervalIntegrable f volume a b ↔ IntervalIntegrable g volume a b := by
-
-  rw [intervalIntegrable_iff_integrableOn_Ioo_of_le hab]
-  rw [MeasureTheory.integrableOn_congr_fun hfg measurableSet_Ioo]
-  rw [← intervalIntegrable_iff_integrableOn_Ioo_of_le hab]
-
-
-
-lemma integral_log_sin₀ : ∫ (x : ℝ) in (0)..π, log (sin x) = 2 * ∫ (x : ℝ) in (0)..(π / 2), log (sin x) := by
-  rw [← intervalIntegral.integral_add_adjacent_intervals (a := 0) (b := π / 2) (c := π)]
-  conv =>
-    left
-    right
-    arg 1
-    intro x
-    rw [← sin_pi_sub]
-  rw [intervalIntegral.integral_comp_sub_left (fun x ↦ log (sin x)) π]
-  have : π - π / 2 = π / 2 := by linarith
-  rw [this]
-  simp
-  ring
-  -- IntervalIntegrable (fun x => log (sin x)) volume 0 (π / 2)
-  exact intervalIntegrable_log_sin₂
-  -- IntervalIntegrable (fun x => log (sin x)) volume (π / 2) π
-  apply intervalIntegrable_log_sin.mono_set
-  rw [Set.uIcc_of_le, Set.uIcc_of_le]
-  apply Set.Icc_subset_Icc_left
-  linarith [pi_pos]
-  linarith [pi_pos]
-  linarith [pi_pos]
-
-
-lemma integral_log_sin₁ : ∫ (x : ℝ) in (0)..(π / 2), log (sin x) = -log 2 * π/2 := by
-
-  have t₁ {x : ℝ} : x ∈ Set.Ioo 0 (π / 2) → log (sin (2 * x)) = log 2 + log (sin x) + log (cos x) := by
-    intro hx
-    simp at hx
-
-    rw [sin_two_mul x, log_mul, log_mul]
-    exact Ne.symm (NeZero.ne' 2)
-    -- sin x ≠ 0
-    apply (fun a => Ne.symm (ne_of_lt a))
-    apply sin_pos_of_mem_Ioo
-    constructor
-    · exact hx.1
-    · linarith [pi_pos, hx.2]
-    -- 2 * sin x ≠ 0
-    simp
-    apply (fun a => Ne.symm (ne_of_lt a))
-    apply sin_pos_of_mem_Ioo
-    constructor
-    · exact hx.1
-    · linarith [pi_pos, hx.2]
-    -- cos x ≠ 0
-    apply (fun a => Ne.symm (ne_of_lt a))
-    apply cos_pos_of_mem_Ioo
-    constructor
-    · linarith [pi_pos, hx.1]
-    · exact hx.2
-
-  have t₂ : Set.EqOn (fun y ↦ log (sin y)) (fun y ↦ log (sin (2 * y)) - log 2 - log (cos y)) (Set.Ioo 0 (π / 2)) := by
-    intro x hx
-    simp
-    rw [t₁ hx]
-    ring
-
-  rw [intervalIntegral.integral_congr_volume _ t₂]
-  rw [intervalIntegral.integral_sub, intervalIntegral.integral_sub]
-  rw [intervalIntegral.integral_const]
-  rw [intervalIntegral.integral_comp_mul_left (c := 2) (f := fun x ↦ log (sin x))]
-  simp
-  have : 2 * (π / 2) = π := by linarith
-  rw [this]
-  rw [integral_log_sin₀]
-
-  have : ∫ (x : ℝ) in (0)..(π / 2), log (sin x) = ∫ (x : ℝ) in (0)..(π / 2), log (cos x) := by
-    conv =>
-      right
-      arg 1
-      intro x
-      rw [← sin_pi_div_two_sub]
-    rw [intervalIntegral.integral_comp_sub_left (fun x ↦ log (sin x)) (π / 2)]
-    simp
-  rw [← this]
-  simp
-  linarith
-
-  exact Ne.symm (NeZero.ne' 2)
-  -- IntervalIntegrable (fun x => log (sin (2 * x))) volume 0 (π / 2)
-  let A := intervalIntegrable_log_sin.comp_mul_left 2
-  simp at A
-  assumption
-  -- IntervalIntegrable (fun x => log 2) volume 0 (π / 2)
-  simp
-  -- IntervalIntegrable (fun x => log (sin (2 * x)) - log 2) volume 0 (π / 2)
-  apply IntervalIntegrable.sub
-  -- -- IntervalIntegrable (fun x => log (sin (2 * x))) volume 0 (π / 2)
-  let A := intervalIntegrable_log_sin.comp_mul_left 2
-  simp at A
-  assumption
-  -- -- IntervalIntegrable (fun x => log 2) volume 0 (π / 2)
-  simp
-  -- -- IntervalIntegrable (fun x => log (cos x)) volume 0 (π / 2)
-  exact intervalIntegrable_log_cos
-  --
-  linarith [pi_pos]
-
-
-lemma integral_log_sin₂ : ∫ (x : ℝ) in (0)..π, log (sin x) = -log 2 * π := by
-  rw [integral_log_sin₀, integral_log_sin₁]
-  ring

Nevanlinna/tensor.lean

@@ -0,0 +1,47 @@
+import Mathlib.Analysis.InnerProductSpace.PiL2
+
+
+open RCLike Real Filter
+open Topology ComplexConjugate
+open LinearMap (BilinForm)
+open TensorProduct
+open InnerProductSpace
+open Inner
+
+
+example
+  {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
+  {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℝ F]
+  : 1 = 0 := by
+
+  let e : E →ₗ[ℝ] E →ₗ[ℝ] ℝ := innerₗ E 
+  let f : F →ₗ[ℝ] F →ₗ[ℝ] ℝ := innerₗ F 
+  let e₂ :=  TensorProduct.map₂ e f
+  let l := TensorProduct.lid ℝ ℝ 
+
+  have : ∀ e1 e2 : E, ∀ f1 f2 : F, e₂ (e1 ⊗ f1) (e2 ⊗ f2) = 
+
+  let X : InnerProductSpace.Core ℝ (E ⊗[ℝ] F) := {
+    inner := by
+      intro a b
+      exact TensorProduct.lid ℝ ℝ ((TensorProduct.map₂ (innerₗ E) (innerₗ F)) a b)
+    conj_symm := by
+      simp
+      intro x y
+
+      unfold innerₗ
+      
+      simp
+      sorry
+    nonneg_re := _
+    definite := _
+    add_left := _
+    smul_left := _
+  }
+
+  let inner : E ⊗[𝕜] E → E ⊗[𝕜] E → 𝕜 := 
+    --let x := TensorProduct.lift
+    --E.inner
+    --TensorProduct.map₂
+    sorry
+  sorry

Nevanlinna/test.lean

@@ -0,0 +1,130 @@
+import Mathlib.Analysis.Complex.CauchyIntegral
+--import Mathlib.Analysis.Complex.Module
+
+
+open ComplexConjugate
+
+#check DiffContOnCl.circleIntegral_sub_inv_smul
+
+open Real
+
+theorem CauchyIntegralFormula :
+  ∀
+  {R : ℝ} -- Radius of the ball
+  {w : ℂ} -- Point in the interior of the ball
+  {f : ℂ → ℂ}, -- Holomorphic function
+  DiffContOnCl ℂ f (Metric.ball 0 R)
+  → w ∈ Metric.ball 0 R
+  → (∮ (z : ℂ) in C(0, R), (z - w)⁻¹ • f z) = (2 * π * Complex.I) • f w := by
+
+  exact DiffContOnCl.circleIntegral_sub_inv_smul
+
+#check CauchyIntegralFormula
+#check HasDerivAt.continuousAt
+#check Real.log
+#check ComplexConjugate.conj
+#check Complex.exp
+
+theorem SimpleCauchyFormula :
+  ∀
+  {R : ℝ} -- Radius of the ball
+  {w : ℂ} -- Point in the interior of the ball
+  {f : ℂ → ℂ}, -- Holomorphic function
+  Differentiable ℂ f
+  → w ∈ Metric.ball 0 R
+  → (∮ (z : ℂ) in C(0, R), (z - w)⁻¹ • f z) = (2 * Real.pi * Complex.I) • f w := by
+
+  intro R w f fHyp
+
+  apply DiffContOnCl.circleIntegral_sub_inv_smul
+
+  constructor
+  · exact Differentiable.differentiableOn fHyp
+  · suffices Continuous f from by
+      exact Continuous.continuousOn this
+    rw [continuous_iff_continuousAt]
+    intro x
+    exact DifferentiableAt.continuousAt (fHyp x)
+
+
+theorem JensenFormula₂ :
+  ∀
+  {R : ℝ} -- Radius of the ball
+  {f : ℂ → ℂ}, -- Holomorphic function
+  Differentiable ℂ f
+  → (∀ z ∈ Metric.ball 0 R, f z ≠ 0)
+  → (∫ (θ : ℝ) in Set.Icc 0 (2 * π), Complex.log ‖f (circleMap 0 R θ)‖ ) = 2 * π * Complex.log ‖f 0‖ := by
+
+  intro r f fHyp₁ fHyp₂
+
+  /- We treat the trivial case r = 0 separately. -/
+  by_cases rHyp : r = 0
+  rw [rHyp]
+  simp
+  left
+  unfold ENNReal.ofReal
+  simp
+  rw [max_eq_left (mul_nonneg zero_le_two pi_nonneg)]
+  simp
+  /- From hereon, we assume that r ≠ 0. -/
+
+  /- Replace the integral over 0 … 2π by a circle integral -/
+  suffices (∮ (z : ℂ) in C(0, r), -(Complex.I * z⁻¹ * Complex.log ↑(Complex.abs (f z)))) = 2 * ↑π * Complex.log ↑‖f 0‖ from by
+    have : ∫ (θ : ℝ) in Set.Icc 0 (2 * π), Complex.log ↑‖f (circleMap 0 r θ)‖ = (∮ (z : ℂ) in C(0, r), -(Complex.I * z⁻¹ * Complex.log ↑(Complex.abs (f z)))) := by
+      have : (fun θ ↦ Complex.log ‖f (circleMap 0 r θ)‖) = (fun θ ↦ ((deriv (circleMap 0 r) θ)) • ((deriv (circleMap 0 r) θ)⁻¹ • Complex.log ↑‖f (circleMap 0 r θ)‖)) := by
+        funext θ
+        rw [← smul_assoc, smul_eq_mul, smul_eq_mul, mul_inv_cancel, one_mul]
+        simp
+        exact rHyp
+      rw [this]
+      simp
+      let tmp := circleIntegral_def_Icc (fun z ↦ -(Complex.I * z⁻¹ * (Complex.log ↑‖f z‖))) 0 r
+      simp at tmp
+      rw [← tmp]
+    rw [this]
+
+  
+
+  have : ∀ z : ℂ, log (Complex.abs z) = 1/2 * Complex.log z + 1/2 * Complex.log (conj z) := by
+    intro z
+
+    by_cases argHyp : Complex.arg z = π 
+    
+    · rw [Complex.log, argHyp, Complex.log]
+      let ZZ := Complex.arg_conj z
+      rw [argHyp] at ZZ
+      
+      simp at ZZ
+
+      have : conj z = z := by
+        apply?
+        sorry
+
+    let ZZ := Complex.log_conj z
+
+    nth_rewrite 1 [Complex.log]
+    
+    simp
+
+    let φ := Complex.arg z
+    let r := Complex.abs z
+    have : z = r * Complex.exp (φ * Complex.I) := by
+      exact (Complex.abs_mul_exp_arg_mul_I z).symm
+
+    have : Complex.log z = Complex.log r + r*Complex.I := by
+      apply?
+      sorry
+    simp at XX
+
+
+    sorry
+
+
+
+
+
+
+
+
+
+  sorry

lake-manifest.json

@@ -1,11 +1,10 @@
-{"version": "1.1.0",
+{"version": "1.0.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "46fed98b5cac2b1ea64e363b420c382ed1af0d85",
+   "rev": "555ec79bc6effe7009036184a5f73f7d8d4850ed",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -14,8 +13,7 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "2c8ae451ce9ffc83554322b14437159c1a9703f9",
+   "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -24,8 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "662f986ad3c5ad6ab1a1726b3c04f5ec425aa9f7",
+   "rev": "30619d94ce4a3d69cdb87bb1771562ca2e687cfa",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -34,48 +31,34 @@
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "eb08eee94098fe530ccd6d8751a86fe405473d4c",
+   "rev": "87c1e7a427d8e21b6eaf8401f12897f52e2c3be9",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.42",
+   "inputRev": "v0.0.38",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "scope": "",
-   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
+   "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/import-graph",
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",
    "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "fb7841a6f4fb389ec0e47dd4677844d49906af3c",
+   "rev": "1588be870b9c76fe62286e8f42f0b4dafa154c96",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/siddhartha-gadgil/LeanSearchClient.git",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "c260ed920e2ebd23ef9fc8ca3fd24115e04c18b1",
-   "name": "LeanSearchClient",
-   "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": "4e40837aec257729b3c38dc3e635fc64a7a8a8c1",
+   "rev": "dcc73cfb2ce3763f830c52042fb8617e762dbf60",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.12.0-rc1
+leanprover/lean4:v4.9.0-rc3