From da859defb1317ef113da0144c18d7c23e82e5a95 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Fri, 9 Aug 2024 10:31:13 +0200 Subject: [PATCH] Update holomorphic_JensenFormula.lean --- Nevanlinna/holomorphic_JensenFormula.lean | 37 +++++++++++++++++++++-- 1 file changed, 34 insertions(+), 3 deletions(-) diff --git a/Nevanlinna/holomorphic_JensenFormula.lean b/Nevanlinna/holomorphic_JensenFormula.lean index ace1ec0..ca56f49 100644 --- a/Nevanlinna/holomorphic_JensenFormula.lean +++ b/Nevanlinna/holomorphic_JensenFormula.lean @@ -33,6 +33,12 @@ lemma int₀ (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 => @@ -58,12 +64,37 @@ lemma int₀ 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 2 , HarmonicAt F x := by - sorry + 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 2 1 Real.zero_lt_one one_lt_two hf + let A := harmonic_meanValue ρ 1 Real.zero_lt_one hρ hf dsimp [F] at A simp at A exact A