From 3063415cf995946a5122051d0549797b5907cb3e Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Wed, 14 Aug 2024 16:03:54 +0200 Subject: [PATCH] Update specialFunctions_Integrals.lean --- Nevanlinna/specialFunctions_Integrals.lean | 132 +++++++++++++++++---- 1 file changed, 109 insertions(+), 23 deletions(-) diff --git a/Nevanlinna/specialFunctions_Integrals.lean b/Nevanlinna/specialFunctions_Integrals.lean index 957bbb8..92dcdc4 100644 --- a/Nevanlinna/specialFunctions_Integrals.lean +++ b/Nevanlinna/specialFunctions_Integrals.lean @@ -9,7 +9,6 @@ open Real Filter MeasureTheory intervalIntegral -- The following theorem was suggested by Gareth Ma on Zulip - lemma logsinBound : ∀ x ∈ (Set.Icc 0 1), ‖(log ∘ sin) x‖ ≤ ‖log ((π / 2)⁻¹ * x)‖ := by intro x hx @@ -18,8 +17,21 @@ lemma logsinBound : ∀ x ∈ (Set.Icc 0 1), ‖(log ∘ sin) x‖ ≤ ‖log (( -- Now handle the case where x ≠ 0 have l₀ : log ((π / 2)⁻¹ * x) ≤ 0 := by - -- log_nonpos (Set.mem_Icc.1 hx).1 (Set.mem_Icc.1 hx).2 - sorry + apply log_nonpos + apply mul_nonneg + apply le_of_lt + apply inv_pos.2 + apply div_pos + exact pi_pos + exact zero_lt_two + apply (Set.mem_Icc.1 hx).1 + simp + apply mul_le_one + rw [div_le_one pi_pos] + exact two_le_pi + exact (Set.mem_Icc.1 hx).1 + exact (Set.mem_Icc.1 hx).2 + have l₁ : 0 ≤ sin x := by apply sin_nonneg_of_nonneg_of_le_pi (Set.mem_Icc.1 hx).1 trans (1 : ℝ) @@ -38,24 +50,6 @@ lemma logsinBound : ∀ x ∈ (Set.Icc 0 1), ‖(log ∘ sin) x‖ ≤ ‖log (( simp exact lt_of_le_of_ne (Set.mem_Icc.1 hx).1 ( fun a => h'x (id (Eq.symm a)) ) - have l₄ : sin x ∈ (Set.Ioi 0) := by - have t₁ : 0 ∈ Set.Icc (-(π / 2)) (π / 2) := by - simp - apply div_nonneg pi_nonneg zero_le_two - have t₂ : x ∈ Set.Icc (-(π / 2)) (π / 2) := by - simp - constructor - · trans 0 - simp - apply div_nonneg pi_nonneg zero_le_two - exact (Set.mem_Icc.1 hx).1 - · trans (1 : ℝ) - exact (Set.mem_Icc.1 hx).2 - exact one_le_pi_div_two - let A := Real.strictMonoOn_sin t₁ t₂ l₃ - simp at A - simpa - have l₅ : 0 < (π / 2)⁻¹ * x := by apply mul_pos apply inv_pos.2 @@ -109,7 +103,7 @@ lemma logsinBound : ∀ x ∈ (Set.Icc 0 1), ‖(log ∘ sin) x‖ ≤ ‖log (( exact one_le_pi_div_two -example : IntervalIntegrable (log ∘ sin) volume 0 1 := by +lemma intervalIntegrable_log_sin₁ : IntervalIntegrable (log ∘ sin) volume 0 1 := by have int_log : IntervalIntegrable (fun x ↦ ‖log x‖) volume 0 1 := by apply IntervalIntegrable.norm @@ -191,6 +185,47 @@ example : IntervalIntegrable (log ∘ sin) volume 0 1 := by exact measurable_log exact measurable_const_mul (π / 2)⁻¹ +lemma intervalIntegrable_log_sin₂ : IntervalIntegrable (log ∘ sin) volume 0 (π / 2) := by + + apply IntervalIntegrable.trans (b := 1) + exact intervalIntegrable_log_sin₁ + + -- IntervalIntegrable (log ∘ sin) volume 1 (π / 2) + apply ContinuousOn.intervalIntegrable + apply ContinuousOn.comp continuousOn_log continuousOn_sin + intro x hx + rw [Set.uIcc_of_le, Set.mem_Icc] at hx + have : 0 < sin x := by + apply Real.sin_pos_of_pos_of_lt_pi + · calc 0 + _ < 1 := Real.zero_lt_one + _ ≤ x := hx.1 + · calc x + _ ≤ π / 2 := hx.2 + _ < π := div_two_lt_of_pos pi_pos + by_contra h₁x + simp at h₁x + rw [h₁x] at this + simp at this + exact one_le_pi_div_two + +lemma intervalIntegrable_log_sin : IntervalIntegrable (log ∘ sin) volume 0 π := by + apply IntervalIntegrable.trans (b := π / 2) + exact intervalIntegrable_log_sin₂ + let A := IntervalIntegrable.comp_sub_left intervalIntegrable_log_sin₂ π + simp at A + let B := IntervalIntegrable.symm A + have : π - π / 2 = π / 2 := by linarith + rwa [this] at B + +lemma intervalIntegrable_log_cos : IntervalIntegrable (log ∘ cos) volume 0 (π / 2) := by + let A := IntervalIntegrable.comp_sub_left intervalIntegrable_log_sin₂ (π / 2) + simp only [Function.comp_apply, sub_zero, sub_self] at A + simp_rw [sin_pi_div_two_sub] at A + have : (fun x => log (cos x)) = log ∘ cos := rfl + apply IntervalIntegrable.symm + rwa [← this] + theorem logInt {t : ℝ} @@ -248,8 +283,59 @@ theorem logInt simp [Set.mem_uIcc, ht] -lemma int₁₁ : ∫ (x : ℝ) in (0)..π, log (4 * sin x ^ 2) = 0 := by +lemma integral_log_sin : ∫ (x : ℝ) in (0)..(π / 2), log (sin x) = -log 2 * π/2 := by + have t₀ {x : ℝ} : sin (2 * x) = 2 * sin x * cos x := sin_two_mul x + + have t₁ {x : ℝ} : log (sin (2 * x)) = log 2 + log (sin x) + log (cos x) := by + rw [sin_two_mul x, log_mul, log_mul] + exact Ne.symm (NeZero.ne' 2) + sorry + sorry + sorry + + have t₂ {x : ℝ} : log (sin x) = log (sin (2 * x)) - log 2 - log (cos x) := by + rw [t₁] + ring + + conv => + left + arg 1 + intro x + rw [t₂] + + rw [intervalIntegral.integral_sub, intervalIntegral.integral_sub] + rw [intervalIntegral.integral_const] + rw [intervalIntegral.integral_comp_mul_left (c := 2) (f := fun x ↦ log (sin x))] + simp + have : 2 * (π / 2) = π := by linarith + rw [this] + + have : ∫ (x : ℝ) in (0)..π, log (sin x) = 2 * ∫ (x : ℝ) in (0)..(π / 2), log (sin x) := by + sorry + rw [this] + have : ∫ (x : ℝ) in (0)..(π / 2), log (sin x) = ∫ (x : ℝ) in (0)..(π / 2), log (cos x) := by + sorry + rw [← this] + simp + linarith + + exact Ne.symm (NeZero.ne' 2) + -- IntervalIntegrable (fun x => log (sin (2 * x))) volume 0 (π / 2) + sorry + -- IntervalIntegrable (fun x => log 2) volume 0 (π / 2) + simp + -- IntervalIntegrable (fun x => log (sin (2 * x)) - log 2) volume 0 (π / 2) + apply IntervalIntegrable.sub + -- -- IntervalIntegrable (fun x => log (sin (2 * x))) volume 0 (π / 2) + sorry + -- -- IntervalIntegrable (fun x => log 2) volume 0 (π / 2) + simp + -- -- IntervalIntegrable (fun x => log (cos x)) volume 0 (π / 2) + exact intervalIntegrable_log_cos + + +lemma int₁₁ : ∫ (x : ℝ) in (0)..π, log (4 * sin x ^ 2) = 0 := by sorry