Nevanlinna/specialFunctions_CircleIntegral_affine.lean

@@ -1,62 +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
-
-
-
-
-lemma int₁₁ : ∫ (x : ℝ) in (0)..π, log (4 * sin x ^ 2) = 0 := by
-  sorry
-
-
-lemma int₁ :
-  ∫ x in (0)..(2 * π), log ‖circleMap 0 1 x - 1‖ = 0 := by
-
-  have {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 * Real.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
-  simp_rw [this]
-  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₁₁

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_Integrals.lean

@@ -6,6 +6,7 @@ import Mathlib.MeasureTheory.Measure.Restrict
 open scoped Interval Topology
 open Real Filter MeasureTheory intervalIntegral
 
+-- The following theorem was suggested by Gareth Ma on Zulip
 
 
 lemma logsinBound : ∀ x ∈ (Set.Icc 0 1), ‖(log ∘ sin) x‖ ≤ ‖log ((π / 2)⁻¹ * x)‖ := by
@@ -226,6 +227,62 @@ lemma intervalIntegrable_log_cos : IntervalIntegrable (log ∘ cos) volume 0 (π
   rwa [← this]
 
 
+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 integral_log_sin : ∫ (x : ℝ) in (0)..(π / 2), log (sin x) =  -log 2 * π/2 := by
 
   have t₀ {x : ℝ} : sin (2 * x) = 2 * sin x * cos x := sin_two_mul x
@@ -276,3 +333,56 @@ lemma integral_log_sin : ∫ (x : ℝ) in (0)..(π / 2), log (sin x) =  -log 2 *
   simp
   -- -- IntervalIntegrable (fun x => log (cos x)) volume 0 (π / 2)
   exact intervalIntegrable_log_cos
+
+
+lemma int₁₁ : ∫ (x : ℝ) in (0)..π, log (4 * sin x ^ 2) = 0 := by
+  sorry
+
+
+lemma int₁ :
+  ∫ x in (0)..(2 * π), log ‖circleMap 0 1 x - 1‖ = 0 := by
+
+  have {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 * Real.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
+  simp_rw [this]
+  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₁₁