From 0cb1914b18f96a61d3781aea1967df273c909ec5 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Tue, 13 Aug 2024 08:42:47 +0200
Subject: [PATCH] Add code of Gareth Ma

---
 Nevanlinna/holomorphic_JensenFormula2.lean |  2 +-
 Nevanlinna/specialFunctions.lean           | 54 -----------------
 Nevanlinna/specialFunctions_Integrals.lean | 68 ++++++++++++++++++++++
 3 files changed, 69 insertions(+), 55 deletions(-)
 delete mode 100644 Nevanlinna/specialFunctions.lean
 create mode 100644 Nevanlinna/specialFunctions_Integrals.lean

diff --git a/Nevanlinna/holomorphic_JensenFormula2.lean b/Nevanlinna/holomorphic_JensenFormula2.lean
index 01003b1..1c2881a 100644
--- a/Nevanlinna/holomorphic_JensenFormula2.lean
+++ b/Nevanlinna/holomorphic_JensenFormula2.lean
@@ -18,7 +18,7 @@ lemma xx
       let A := hf z hz
       let B := A.order
 
-      exact A.order
+      exact (A.order : ⊤)
     else
       exact 0
 
diff --git a/Nevanlinna/specialFunctions.lean b/Nevanlinna/specialFunctions.lean
deleted file mode 100644
index 27dfe04..0000000
--- a/Nevanlinna/specialFunctions.lean
+++ /dev/null
@@ -1,54 +0,0 @@
-import Mathlib.Analysis.SpecialFunctions.Integrals
-
-theorem intervalIntegral.intervalIntegrable_log'
-  {a : ℝ}
-  {b : ℝ}
-  {μ : MeasureTheory.Measure ℝ}
-  [MeasureTheory.IsLocallyFiniteMeasure μ]
-  (ha : 0 < a) :
-  IntervalIntegrable Real.log μ 0 a
-  := by
-
-  sorry
-
-theorem integral_log₀
-  {b : ℝ}
-  (hb : 0 < b) :
-  ∫ (x : ℝ) in (0)..b, Real.log x = b * (Real.log b - 1) := by
-  apply?
-  exact integral_log h
-
-
-open Real Nat Set Finset
-
-open scoped Real Interval
-
---variable {a b : ℝ} (n : ℕ)
-
-namespace intervalIntegral
-
---open MeasureTheory
-
---variable {f : ℝ → ℝ} {μ ν : Measure ℝ} [IsLocallyFiniteMeasure μ] (c d : ℝ)
-
-#check integral_mul_deriv_eq_deriv_mul
-
-theorem integral_log₁
-  (h : (0 : ℝ) ∉ [[a, b]]) :
-  ∫ x in a..b, log x = b * log b - a * log a - b + a := by
-
-  have h' : ∀ x ∈ [[a, b]], x ≠ 0 :=
-    fun x (hx : x ∈ [[a, b]]) => ne_of_mem_of_not_mem hx h
-  have heq :  ∀ x ∈ [[a, b]], x * x⁻¹ = 1 :=
-    fun x hx => mul_inv_cancel (h' x hx)
-
-  let A := fun x hx => hasDerivAt_log (h' x hx)
-
-  convert integral_mul_deriv_eq_deriv_mul A (fun x _ => hasDerivAt_id x)
-
-  convert integral_mul_deriv_eq_deriv_mul A
-    (fun x _ => hasDerivAt_id x) (continuousOn_inv₀.mono <|
-      subset_compl_singleton_iff.mpr h).intervalIntegrable
-        continuousOn_const.intervalIntegrable using 1 <;>
-
-  simp [integral_congr heq, mul_comm, ← sub_add]
diff --git a/Nevanlinna/specialFunctions_Integrals.lean b/Nevanlinna/specialFunctions_Integrals.lean
new file mode 100644
index 0000000..13dad97
--- /dev/null
+++ b/Nevanlinna/specialFunctions_Integrals.lean
@@ -0,0 +1,68 @@
+import Mathlib.Analysis.SpecialFunctions.Integrals
+import Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
+import Mathlib.MeasureTheory.Integral.CircleIntegral
+
+open scoped Interval Topology
+open Real Filter MeasureTheory intervalIntegral
+
+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]
+
+
+lemma int₁ :
+  ∫ x in (0)..(2 * π), log ‖circleMap 0 1 x - 1‖ = 0 := by
+  dsimp [circleMap]
+
+  sorry