working…

Nevanlinna/harmonicAt.lean

@@ -47,6 +47,24 @@ theorem HarmonicAt_iff
       · apply (IsOpen.mem_nhds_iff h₁s).2 h₂s
       · exact h₂f
 
+theorem HarmonicAt_isOpen
+  (f : ℂ → F) :
+  IsOpen { x : ℂ | HarmonicAt f x } := by
+
+  rw [← subset_interior_iff_isOpen]
+  intro x hx
+  simp at hx
+  obtain ⟨s, h₁s, h₂s, h₃s⟩ := HarmonicAt_iff.1 hx
+  use s
+  constructor
+  · simp
+    constructor
+    · exact h₁s
+    · intro x hx
+      simp
+      rw [HarmonicAt_iff]
+      use s
+  · exact h₂s
 
 theorem HarmonicAt_eventuallyEq {f₁ f₂ : ℂ → F} {x : ℂ} (h : f₁ =ᶠ[nhds x] f₂) : HarmonicAt f₁ x ↔ HarmonicAt f₂ x := by
   constructor

Nevanlinna/harmonicAt_examples.lean

@@ -1,5 +1,5 @@
 import Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
-import Nevanlinna.complexHarmonic
+import Nevanlinna.harmonicAt
 import Nevanlinna.holomorphicAt
 
 variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F]

Nevanlinna/harmonicAt_meanValue.lean

@@ -1,3 +1,5 @@
+import Mathlib.Analysis.NormedSpace.Pointwise
+import Mathlib.Topology.MetricSpace.Thickening
 import Mathlib.Analysis.Complex.CauchyIntegral
 import Nevanlinna.holomorphic_examples
 
@@ -104,3 +106,26 @@ theorem harmonic_meanValue
   rwa [abs_of_nonneg (le_of_lt hR)]
   apply Continuous.continuousOn
   exact continuous_circleMap z R
+
+/- Probably not optimal yet. We want a statements that requires harmonicity in
+the interior and continuity on the closed ball.
+-/
+
+
+theorem harmonic_meanValue₁
+  {f : ℂ → ℝ}
+  {z : ℂ}
+  (R : ℝ)
+  (hR : 0 < R)
+  (hf : ∀ x ∈ Metric.closedBall z R , HarmonicAt f x) :
+  (∫ (x : ℝ) in (0)..2 * Real.pi, f (circleMap z R x)) = 2 * Real.pi * f z := by
+
+  obtain ⟨e, h₁e, h₂e⟩ := IsCompact.exists_thickening_subset_open (isCompact_closedBall z R) (HarmonicAt_isOpen f) hf
+  rw [thickening_closedBall] at h₂e
+  apply harmonic_meanValue (e + R) R
+  assumption
+  norm_num
+  assumption
+  exact fun x a => h₂e a
+  assumption
+  linarith

Nevanlinna/holomorphic_JensenFormula.lean

@@ -1,110 +1,6 @@
 import Nevanlinna.harmonicAt_examples
 import Nevanlinna.harmonicAt_meanValue
-
-lemma l₀ {x₁ x₂ : ℝ} : (circleMap 0 1 x₁) * (circleMap 0 1 x₂) = circleMap 0 1 (x₁+x₂) := by
-  dsimp [circleMap]
-  simp
-  rw [add_mul, Complex.exp_add]
-
-lemma l₁ {x : ℝ} : ‖circleMap 0 1 x‖ = 1 := by
-  rw [Complex.norm_eq_abs, abs_circleMap_zero]
-  simp
-
-lemma l₂ {x : ℝ} : ‖(circleMap 0 1 x) - a‖ = ‖1 - (circleMap 0 1 (-x)) * a‖ := by
-  calc ‖(circleMap 0 1 x) - a‖
-  _ = 1 * ‖(circleMap 0 1 x) - a‖ := by
-    exact Eq.symm (one_mul ‖circleMap 0 1 x - a‖)
-  _ = ‖(circleMap 0 1 (-x))‖ * ‖(circleMap 0 1 x) - a‖ := by
-    rw [l₁]
-  _ = ‖(circleMap 0 1 (-x)) * ((circleMap 0 1 x) - a)‖ := by
-    exact Eq.symm (NormedField.norm_mul' (circleMap 0 1 (-x)) (circleMap 0 1 x - a))
-  _ = ‖(circleMap 0 1 (-x)) * (circleMap 0 1 x) - (circleMap 0 1 (-x)) * a‖ := by
-    rw [mul_sub]
-  _ = ‖(circleMap 0 1 0) - (circleMap 0 1 (-x)) * a‖ := by
-    rw [l₀]
-    simp
-  _ = ‖1 - (circleMap 0 1 (-x)) * a‖ := by
-    congr
-    dsimp [circleMap]
-    simp
-
-lemma int₀
-  {a : ℂ}
-  (ha : a ∈ Metric.ball 0 1) :
-  ∫ (x : ℝ) in (0)..2 * Real.pi, Real.log ‖circleMap 0 1 x - a‖ = 0 := by
-
-  by_cases h₁a : a = 0
-  · -- case: a = 0
-    rw [h₁a]
-    simp
-
-  -- case: a ≠ 0
-  simp_rw [l₂]
-  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 ↦ Real.log ‖1 - circleMap 0 1 (w) * a‖))]
-
-  let f₁ := fun w ↦ Real.log ‖1 - circleMap 0 1 w * a‖
-  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
-    simp at A
-    exact id (Eq.symm A)
-  conv =>
-    left
-    arg 1
-    intro x
-    rw [this]
-  rw [intervalIntegral.integral_comp_add_right f₁ (2 * Real.pi)]
-  simp
-  dsimp [f₁]
-
-  let ρ := ‖a‖⁻¹
-  have hρ : 1 < ρ := by
-    apply one_lt_inv_iff.mpr
-    constructor
-    · exact norm_pos_iff'.mpr h₁a
-    · exact mem_ball_zero_iff.mp ha
-
-  let F := fun z ↦ Real.log ‖1 - z * a‖
-
-  have hf : ∀ x ∈ Metric.ball 0 ρ, HarmonicAt F x := by
-    intro x hx
-    apply logabs_of_holomorphicAt_is_harmonic
-    apply Differentiable.holomorphicAt
-    fun_prop
-    apply sub_ne_zero_of_ne
-    by_contra h
-    have : ‖x * a‖ < 1 := by
-      calc ‖x * a‖
-      _ = ‖x‖ * ‖a‖ := by exact NormedField.norm_mul' x a
-      _ < ρ * ‖a‖ := by
-        apply (mul_lt_mul_right _).2
-        exact mem_ball_zero_iff.mp hx
-        exact norm_pos_iff'.mpr h₁a
-      _ = 1 := by
-        dsimp [ρ]
-        apply inv_mul_cancel
-        exact (AbsoluteValue.ne_zero_iff Complex.abs).mpr h₁a
-    rw [← h] at this
-    simp at this
-
-  let A := harmonic_meanValue ρ 1 Real.zero_lt_one hρ hf
-  dsimp [F] at A
-  simp at A
-  exact A
-
-
-lemma int₁ :
-  ∫ (x : ℝ) in (0)..2 * Real.pi, Real.log ‖circleMap 0 1 x - 1‖ = 0 := by
-  dsimp [circleMap]
-
-  sorry
+import Nevanlinna.specialFunctions_CircleIntegral_affine
 
 
 theorem jensen_case_R_eq_one

Nevanlinna/holomorphic_examples.lean

@@ -1,4 +1,4 @@
-import Nevanlinna.complexHarmonic
+import Nevanlinna.harmonicAt
 import Nevanlinna.holomorphicAt
 import Nevanlinna.holomorphic_primitive
 import Nevanlinna.mathlibAddOn

Nevanlinna/specialFunctions_CircleIntegral_affine.lean

@@ -1,14 +1,112 @@
-import Mathlib.Analysis.SpecialFunctions.Integrals
-import Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
+import Mathlib.MeasureTheory.Integral.Periodic
 import Mathlib.MeasureTheory.Integral.CircleIntegral
-import Mathlib.MeasureTheory.Measure.Restrict
 import Nevanlinna.specialFunctions_Integral_log_sin
+import Nevanlinna.harmonicAt_examples
+import Nevanlinna.harmonicAt_meanValue
 
 open scoped Interval Topology
 open Real Filter MeasureTheory intervalIntegral
 
 
 
+lemma l₀ {x₁ x₂ : ℝ} : (circleMap 0 1 x₁) * (circleMap 0 1 x₂) = circleMap 0 1 (x₁+x₂) := by
+  dsimp [circleMap]
+  simp
+  rw [add_mul, Complex.exp_add]
+
+lemma l₁ {x : ℝ} : ‖circleMap 0 1 x‖ = 1 := by
+  rw [Complex.norm_eq_abs, abs_circleMap_zero]
+  simp
+
+lemma l₂ {x : ℝ} : ‖(circleMap 0 1 x) - a‖ = ‖1 - (circleMap 0 1 (-x)) * a‖ := by
+  calc ‖(circleMap 0 1 x) - a‖
+  _ = 1 * ‖(circleMap 0 1 x) - a‖ := by
+    exact Eq.symm (one_mul ‖circleMap 0 1 x - a‖)
+  _ = ‖(circleMap 0 1 (-x))‖ * ‖(circleMap 0 1 x) - a‖ := by
+    rw [l₁]
+  _ = ‖(circleMap 0 1 (-x)) * ((circleMap 0 1 x) - a)‖ := by
+    exact Eq.symm (NormedField.norm_mul' (circleMap 0 1 (-x)) (circleMap 0 1 x - a))
+  _ = ‖(circleMap 0 1 (-x)) * (circleMap 0 1 x) - (circleMap 0 1 (-x)) * a‖ := by
+    rw [mul_sub]
+  _ = ‖(circleMap 0 1 0) - (circleMap 0 1 (-x)) * a‖ := by
+    rw [l₀]
+    simp
+  _ = ‖1 - (circleMap 0 1 (-x)) * a‖ := by
+    congr
+    dsimp [circleMap]
+    simp
+
+lemma int₀
+  {a : ℂ}
+  (ha : a ∈ Metric.ball 0 1) :
+  ∫ (x : ℝ) in (0)..2 * Real.pi, Real.log ‖circleMap 0 1 x - a‖ = 0 := by
+
+  by_cases h₁a : a = 0
+  · -- case: a = 0
+    rw [h₁a]
+    simp
+
+  -- case: a ≠ 0
+  simp_rw [l₂]
+  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 ↦ Real.log ‖1 - circleMap 0 1 (w) * a‖))]
+
+  let f₁ := fun w ↦ Real.log ‖1 - circleMap 0 1 w * a‖
+  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
+    simp at A
+    exact id (Eq.symm A)
+  conv =>
+    left
+    arg 1
+    intro x
+    rw [this]
+  rw [intervalIntegral.integral_comp_add_right f₁ (2 * Real.pi)]
+  simp
+  dsimp [f₁]
+
+  let ρ := ‖a‖⁻¹
+  have hρ : 1 < ρ := by
+    apply one_lt_inv_iff.mpr
+    constructor
+    · exact norm_pos_iff'.mpr h₁a
+    · exact mem_ball_zero_iff.mp ha
+
+  let F := fun z ↦ Real.log ‖1 - z * a‖
+
+  have hf : ∀ x ∈ Metric.ball 0 ρ, HarmonicAt F x := by
+    intro x hx
+    apply logabs_of_holomorphicAt_is_harmonic
+    apply Differentiable.holomorphicAt
+    fun_prop
+    apply sub_ne_zero_of_ne
+    by_contra h
+    have : ‖x * a‖ < 1 := by
+      calc ‖x * a‖
+      _ = ‖x‖ * ‖a‖ := by exact NormedField.norm_mul' x a
+      _ < ρ * ‖a‖ := by
+        apply (mul_lt_mul_right _).2
+        exact mem_ball_zero_iff.mp hx
+        exact norm_pos_iff'.mpr h₁a
+      _ = 1 := by
+        dsimp [ρ]
+        apply inv_mul_cancel
+        exact (AbsoluteValue.ne_zero_iff Complex.abs).mpr h₁a
+    rw [← h] at this
+    simp at this
+
+  let A := harmonic_meanValue ρ 1 Real.zero_lt_one hρ hf
+  dsimp [F] at A
+  simp at A
+  exact A
+
 
 lemma int₁₁ : ∫ (x : ℝ) in (0)..π, log (4 * sin x ^ 2) = 0 := by
 
@@ -91,3 +189,63 @@ lemma int₁ :
   rw [this]
   simp
   exact int₁₁
+
+
+lemma int₂
+  {a : ℂ}
+  (ha : ‖a‖ = 1) :
+  ∫ x in (0)..(2 * Real.pi), log ‖circleMap 0 1 x - a‖ = 0 := by
+
+  simp_rw [l₂]
+  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 ↦ Real.log ‖1 - circleMap 0 1 (w) * a‖))]
+
+  let f₁ := fun w ↦ Real.log ‖1 - circleMap 0 1 w * a‖
+  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
+    simp at A
+    exact id (Eq.symm A)
+  conv =>
+    left
+    arg 1
+    intro x
+    rw [this]
+  rw [intervalIntegral.integral_comp_add_right f₁ (2 * Real.pi)]
+  simp
+  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₀]
+
+  rw [intervalIntegral.integral_comp_add_right (f := fun x ↦ log (Complex.abs (1 - circleMap 0 1 (x))))]
+
+  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 := Function.Periodic.intervalIntegral_add_eq this ζ 0
+  simp at A
+  simp
+  rw [add_comm]
+  rw [A]
+
+  have {x : ℝ} : log (Complex.abs (1 - circleMap 0 1 x)) = log ‖circleMap 0 1 x - 1‖ := by
+    rw [← AbsoluteValue.map_neg Complex.abs]
+    simp
+  simp_rw [this]
+  exact int₁

Nevanlinna/specialFunctions_Integral_log_sin.lean

@@ -254,6 +254,31 @@ theorem intervalIntegral.integral_congr_volume
   _ = 0 := volume_singleton
 
 
+
+lemma integral_log_sin₀ : ∫ (x : ℝ) in (0)..π, log (sin x) = 2 * ∫ (x : ℝ) in (0)..(π / 2), log (sin x) := by
+  rw [← intervalIntegral.integral_add_adjacent_intervals (a := 0) (b := π / 2) (c := π)]
+  conv =>
+    left
+    right
+    arg 1
+    intro x
+    rw [← sin_pi_sub]
+  rw [intervalIntegral.integral_comp_sub_left (fun x ↦ log (sin x)) π]
+  have : π - π / 2 = π / 2 := by linarith
+  rw [this]
+  simp
+  ring
+  -- IntervalIntegrable (fun x => log (sin x)) volume 0 (π / 2)
+  exact intervalIntegrable_log_sin₂
+  -- IntervalIntegrable (fun x => log (sin x)) volume (π / 2) π
+  apply intervalIntegrable_log_sin.mono_set
+  rw [Set.uIcc_of_le, Set.uIcc_of_le]
+  apply Set.Icc_subset_Icc_left
+  linarith [pi_pos]
+  linarith [pi_pos]
+  linarith [pi_pos]
+
+
 lemma integral_log_sin₁ : ∫ (x : ℝ) in (0)..(π / 2), log (sin x) = -log 2 * π/2 := by
 
   have t₁ {x : ℝ} : x ∈ Set.Ioo 0 (π / 2) → log (sin (2 * x)) = log 2 + log (sin x) + log (cos x) := by
@@ -295,30 +320,7 @@ lemma integral_log_sin₁ : ∫ (x : ℝ) in (0)..(π / 2), log (sin x) =  -log
   simp
   have : 2 * (π / 2) = π := by linarith
   rw [this]
-
-  have : ∫ (x : ℝ) in (0)..π, log (sin x) = 2 * ∫ (x : ℝ) in (0)..(π / 2), log (sin x) := by
-    rw [← intervalIntegral.integral_add_adjacent_intervals (a := 0) (b := π / 2) (c := π)]
-    conv =>
-      left
-      right
-      arg 1
-      intro x
-      rw [← sin_pi_sub]
-    rw [intervalIntegral.integral_comp_sub_left (fun x ↦ log (sin x)) π]
-    have : π - π / 2 = π / 2 := by linarith
-    rw [this]
-    simp
-    ring
-    -- IntervalIntegrable (fun x => log (sin x)) volume 0 (π / 2)
-    exact intervalIntegrable_log_sin₂
-    -- IntervalIntegrable (fun x => log (sin x)) volume (π / 2) π
-    apply intervalIntegrable_log_sin.mono_set
-    rw [Set.uIcc_of_le, Set.uIcc_of_le]
-    apply Set.Icc_subset_Icc_left
-    linarith [pi_pos]
-    linarith [pi_pos]
-    linarith [pi_pos]
-  rw [this]
+  rw [integral_log_sin₀]
 
   have : ∫ (x : ℝ) in (0)..(π / 2), log (sin x) = ∫ (x : ℝ) in (0)..(π / 2), log (cos x) := by
     conv =>
@@ -354,4 +356,5 @@ lemma integral_log_sin₁ : ∫ (x : ℝ) in (0)..(π / 2), log (sin x) =  -log
 
 
 lemma integral_log_sin₂ : ∫ (x : ℝ) in (0)..π, log (sin x) = -log 2 * π := by
-  sorry
+  rw [integral_log_sin₀, integral_log_sin₁]
+  ring