Working…

Nevanlinna/harmonicAt_meanValue.lean

@@ -7,8 +7,7 @@ theorem harmonic_meanValue
   (ρ R : ℝ)
   (hR : 0 < R)
   (hρ : R < ρ)
-  (hf : ∀ x ∈ Metric.ball z ρ , HarmonicAt f x)
-  :
+  (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
 

Nevanlinna/specialFunctions_Integrals.lean

@@ -1,12 +1,57 @@
 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
 
+example : IntervalIntegrable (log ∘ sin) volume 0 1 := by
+
+  have int_log : IntervalIntegrable log volume 0 1 := by sorry
+
+  apply IntervalIntegrable.mono_fun' (g := log)
+
+  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] at hx
+  rw [Set.left_mem_uIoc] at hx
+  linarith
+  exact continuousOn_sin
+  --
+  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⟩
+  --
+  exact measurableSet_uIoc
+  --
+
+  have : ∀ x ∈ (Ι 0 1), ‖(log ∘ sin) x‖ ≤ log x := by sorry
+  dsimp [EventuallyLE]
+  rw [MeasureTheory.ae_restrict_iff]
+  apply MeasureTheory.ae_of_all
+  exact this
+
+  --intro x
+  rw [MeasureTheory.ae_iff]
+  simp
+
+  rw [MeasureTheory.ae_iff]
+  simp
+
+
+  sorry
+
+
 theorem logInt
   {t : ℝ}
   (ht : 0 < t) :
@@ -63,6 +108,11 @@ theorem logInt
     simp [Set.mem_uIcc, ht]
 
 
+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
 
@@ -109,7 +159,4 @@ lemma int₁ :
     simp
   rw [this]
   simp
-
-
-
-  sorry
+  exact int₁₁