Nevanlinna/holomorphic_JensenFormula2.lean

@@ -3,7 +3,6 @@ import Mathlib.Analysis.Analytic.IsolatedZeros
 import Nevanlinna.analyticOn_zeroSet
 import Nevanlinna.harmonicAt_examples
 import Nevanlinna.harmonicAt_meanValue
-import Nevanlinna.specialFunctions_CircleIntegral_affine
 
 open Real
 
@@ -89,7 +88,6 @@ theorem jensen_case_R_eq_one
     tauto
 
   have : ∫ (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
@@ -135,16 +133,11 @@ theorem jensen_case_R_eq_one
 
     --  ∀ i ∈ (ZeroFinset h₁f).attach, IntervalIntegrable (fun x => ↑(order i) *
     --  log (Complex.abs (circleMap 0 1 x - ↑i))) MeasureTheory.volume 0 (2 * π)
+
+    -- This won't work, because the function **is not** continuous. Need to fix.
     intro i hi
     apply IntervalIntegrable.const_mul
-    have : i.1 ∈ Metric.closedBall (0 : ℂ) 1 := by exact ((ZeroFinset_mem_iff h₁f i).1 i.2).1
+    exact h₁Gi i hi
-    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
@@ -157,73 +150,14 @@ theorem jensen_case_R_eq_one
     simp
 
     by_contra ha'
-    conv at h₂i =>
+    let A := ha i
-      arg 1
+    rw [← ha'] at A
-      rw [← ha']
+    simp at A
-      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]
-    --
-    apply ContinuousAt.comp
-    apply Complex.continuous_abs.continuousAt
-    apply ContinuousAt.comp
-    apply DifferentiableAt.continuousAt (𝕜 := ℂ )
-    apply HolomorphicAt.differentiableAt
-    simp [h₁F]
-    --
-    apply Continuous.continuousAt
-    apply continuous_circleMap
-    --
-    have : (fun x => ∑ s ∈ (ZeroFinset h₁f).attach, ↑(order s) * log (Complex.abs (circleMap 0 1 x - ↑s)))
-      = ∑ s ∈ (ZeroFinset h₁f).attach, (fun x => ↑(order s) * log (Complex.abs (circleMap 0 1 x - ↑s))) := by
-      funext x
-      simp
-    rw [this]
-    apply IntervalIntegrable.sum
-    intro i h₂i
-    apply IntervalIntegrable.const_mul
-    have : i.1 ∈ Metric.closedBall (0 : ℂ) 1 := by exact ((ZeroFinset_mem_iff h₁f i).1 i.2).1
-    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'
+    sorry
-    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
 
 
   sorry

Nevanlinna/periodic_integrability.lean

@@ -1,109 +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 Mathlib.Algebra.Periodic
-
-open scoped Interval Topology
-open Real Filter MeasureTheory intervalIntegral
-
-
-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/specialFunctions_CircleIntegral_affine.lean

@@ -3,19 +3,12 @@ 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
 
--- Integrability of periodic functions
 
 
-
-
-
--- 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
@@ -58,16 +51,16 @@ lemma int₀
 
   -- 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
+  have {x : ℝ} : Real.log ‖1 - circleMap 0 1 (-x) * a‖ = (fun w ↦ Real.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‖))]
+  rw [intervalIntegral.integral_comp_neg ((fun w ↦ Real.log ‖1 - circleMap 0 1 (w) * a‖))]
 
-  let f₁ := fun w ↦ log ‖1 - circleMap 0 1 w * a‖
+  let f₁ := fun w ↦ Real.log ‖1 - circleMap 0 1 w * a‖
-  have {x : ℝ} : log ‖1 - circleMap 0 1 x * a‖ = f₁ (x + 2 * π) := by
+  have {x : ℝ} : Real.log ‖1 - circleMap 0 1 x * a‖ = f₁ (x + 2 * Real.pi) := by
     dsimp [f₁]
     congr 4
     let A := periodic_circleMap 0 1 x
@@ -78,7 +71,7 @@ lemma int₀
     arg 1
     intro x
     rw [this]
-  rw [intervalIntegral.integral_comp_add_right f₁ (2 * π)]
+  rw [intervalIntegral.integral_comp_add_right f₁ (2 * Real.pi)]
   simp
   dsimp [f₁]
 
@@ -89,7 +82,7 @@ lemma int₀
     · exact norm_pos_iff'.mpr h₁a
     · exact mem_ball_zero_iff.mp ha
 
-  let F := fun z ↦ log ‖1 - z * a‖
+  let F := fun z ↦ Real.log ‖1 - z * a‖
 
   have hf : ∀ x ∈ Metric.ball 0 ρ, HarmonicAt F x := by
     intro x hx
@@ -112,7 +105,7 @@ lemma int₀
     rw [← h] at this
     simp at this
 
-  let A := harmonic_meanValue ρ 1 zero_lt_one hρ hf
+  let A := harmonic_meanValue ρ 1 Real.zero_lt_one hρ hf
   dsimp [F] at A
   simp at A
   exact A
@@ -170,7 +163,7 @@ lemma logAffineHelper {x : ℝ} : log ‖circleMap 0 1 x - 1‖ = log (4 * sin (
   _ = 2 - 2 * cos (2 * (x / 2)) := by
     rw [← mul_div_assoc]
     congr; norm_num
-  _ = 4 - 4 * cos (x / 2) ^ 2 := by
+  _ = 4 - 4 * Real.cos (x / 2) ^ 2 := by
     rw [cos_two_mul]
     ring
   _ = 4 * sin (x / 2) ^ 2 := by
@@ -179,36 +172,11 @@ lemma logAffineHelper {x : ℝ} : log ‖circleMap 0 1 x - 1‖ = log (4 * sin (
 
 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
+  sorry
-    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₁ :
@@ -237,87 +205,22 @@ lemma int₁ :
   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
+  ∫ x in (0)..(2 * Real.pi), 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
+  have {x : ℝ} : Real.log ‖1 - circleMap 0 1 (-x) * a‖ = (fun w ↦ Real.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‖))]
+  rw [intervalIntegral.integral_comp_neg ((fun w ↦ Real.log ‖1 - circleMap 0 1 (w) * a‖))]
 
-  let f₁ := fun w ↦ log ‖1 - circleMap 0 1 w * a‖
+  let f₁ := fun w ↦ Real.log ‖1 - circleMap 0 1 w * a‖
-  have {x : ℝ} : log ‖1 - circleMap 0 1 x * a‖ = f₁ (x + 2 * π) := by
+  have {x : ℝ} : Real.log ‖1 - circleMap 0 1 x * a‖ = f₁ (x + 2 * Real.pi) := by
     dsimp [f₁]
     congr 4
     let A := periodic_circleMap 0 1 x
@@ -328,7 +231,7 @@ lemma int₂
     arg 1
     intro x
     rw [this]
-  rw [intervalIntegral.integral_comp_add_right f₁ (2 * π)]
+  rw [intervalIntegral.integral_comp_add_right f₁ (2 * Real.pi)]
   simp
   dsimp [f₁]