From e6f60971a83b0855d8dc4171571cfdbfbf66b951 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Mon, 12 Aug 2024 13:01:35 +0200
Subject: [PATCH] =?UTF-8?q?Working=E2=80=A6?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Nevanlinna/holomorphic_JensenFormula.lean  |  7 +++
 Nevanlinna/holomorphic_JensenFormula2.lean |  0
 Nevanlinna/specialFunctions.lean           | 54 ++++++++++++++++++++++
 3 files changed, 61 insertions(+)
 create mode 100644 Nevanlinna/holomorphic_JensenFormula2.lean
 create mode 100644 Nevanlinna/specialFunctions.lean

diff --git a/Nevanlinna/holomorphic_JensenFormula.lean b/Nevanlinna/holomorphic_JensenFormula.lean
index ca56f49..9aaf160 100644
--- a/Nevanlinna/holomorphic_JensenFormula.lean
+++ b/Nevanlinna/holomorphic_JensenFormula.lean
@@ -100,6 +100,13 @@ lemma int₀
   exact A
 
 
+lemma int₁ :
+  ∫ (x : ℝ) in (0)..2 * Real.pi, Real.log ‖circleMap 0 1 x - 1‖ = 0 := by
+  dsimp [circleMap]
+
+  sorry
+
+
 theorem jensen_case_R_eq_one
   (f : ℂ → ℂ)
   (h₁f : Differentiable ℂ f)
diff --git a/Nevanlinna/holomorphic_JensenFormula2.lean b/Nevanlinna/holomorphic_JensenFormula2.lean
new file mode 100644
index 0000000..e69de29
diff --git a/Nevanlinna/specialFunctions.lean b/Nevanlinna/specialFunctions.lean
new file mode 100644
index 0000000..27dfe04
--- /dev/null
+++ b/Nevanlinna/specialFunctions.lean
@@ -0,0 +1,54 @@
+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]