From 371b90c1c6434d0b36edb9bc3c873edefc38cf20 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Thu, 22 Aug 2024 13:09:03 +0200 Subject: [PATCH] =?UTF-8?q?working=E2=80=A6?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Nevanlinna/holomorphic_JensenFormula2.lean | 82 +++++++++++-- Nevanlinna/periodic_integrability.lean | 109 ++++++++++++++++++ ...pecialFunctions_CircleIntegral_affine.lean | 89 ++++++++++++++ 3 files changed, 272 insertions(+), 8 deletions(-) create mode 100644 Nevanlinna/periodic_integrability.lean diff --git a/Nevanlinna/holomorphic_JensenFormula2.lean b/Nevanlinna/holomorphic_JensenFormula2.lean index b295282..59c7a60 100644 --- a/Nevanlinna/holomorphic_JensenFormula2.lean +++ b/Nevanlinna/holomorphic_JensenFormula2.lean @@ -3,6 +3,7 @@ import Mathlib.Analysis.Analytic.IsolatedZeros import Nevanlinna.analyticOn_zeroSet import Nevanlinna.harmonicAt_examples import Nevanlinna.harmonicAt_meanValue +import Nevanlinna.specialFunctions_CircleIntegral_affine open Real @@ -88,6 +89,7 @@ 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 @@ -133,11 +135,16 @@ 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 - exact h₁Gi i hi + 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 @@ -150,14 +157,73 @@ theorem jensen_case_R_eq_one simp by_contra ha' - let A := ha i - rw [← ha'] at A - simp at A + 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 + -- 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' + 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 - sorry diff --git a/Nevanlinna/periodic_integrability.lean b/Nevanlinna/periodic_integrability.lean new file mode 100644 index 0000000..7e26451 --- /dev/null +++ b/Nevanlinna/periodic_integrability.lean @@ -0,0 +1,109 @@ +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 diff --git a/Nevanlinna/specialFunctions_CircleIntegral_affine.lean b/Nevanlinna/specialFunctions_CircleIntegral_affine.lean index d67a0d3..69f381e 100644 --- a/Nevanlinna/specialFunctions_CircleIntegral_affine.lean +++ b/Nevanlinna/specialFunctions_CircleIntegral_affine.lean @@ -3,12 +3,19 @@ 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 @@ -187,6 +194,23 @@ lemma int'₁ : -- Integrability of log ‖circleMap 0 1 x - 1‖ 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₁ : ∫ x in (0)..(2 * π), log ‖circleMap 0 1 x - 1‖ = 0 := by @@ -213,6 +237,71 @@ 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) :