From 10f88298c09fd3f588cb723693eb22576b872790 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Thu, 15 Aug 2024 11:46:19 +0200 Subject: [PATCH] Update specialFunctions_Integral_log_sin.lean --- .../specialFunctions_Integral_log_sin.lean | 114 +++++++++++++++--- 1 file changed, 95 insertions(+), 19 deletions(-) diff --git a/Nevanlinna/specialFunctions_Integral_log_sin.lean b/Nevanlinna/specialFunctions_Integral_log_sin.lean index e4423a3..3153c09 100644 --- a/Nevanlinna/specialFunctions_Integral_log_sin.lean +++ b/Nevanlinna/specialFunctions_Integral_log_sin.lean @@ -208,16 +208,17 @@ lemma intervalIntegrable_log_sin₂ : IntervalIntegrable (log ∘ sin) volume 0 simp at this exact one_le_pi_div_two -lemma intervalIntegrable_log_sin : IntervalIntegrable (log ∘ sin) volume 0 π := by +theorem intervalIntegrable_log_sin : IntervalIntegrable (log ∘ sin) volume 0 π := by apply IntervalIntegrable.trans (b := π / 2) exact intervalIntegrable_log_sin₂ + -- IntervalIntegrable (log ∘ sin) volume (π / 2) π 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 +theorem 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 @@ -225,28 +226,70 @@ lemma intervalIntegrable_log_cos : IntervalIntegrable (log ∘ cos) volume 0 (π apply IntervalIntegrable.symm rwa [← this] +theorem intervalIntegral.integral_congr_volume + {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] + {f : ℝ → E} + {g : ℝ → E} + {a : ℝ} + {b : ℝ} + (h₀ : a < b) + (h₁ : Set.EqOn f g (Set.Ioo a b)) : + ∫ (x : ℝ) in a..b, f x = ∫ (x : ℝ) in a..b, g x := by + + apply intervalIntegral.integral_congr_ae + rw [MeasureTheory.ae_iff] + apply nonpos_iff_eq_zero.1 + push_neg + have : {x | x ∈ Ι a b ∧ f x ≠ g x} ⊆ {b} := by + intro x hx + have t₂ : x ∈ Ι a b \ Set.Ioo a b := by + constructor + · exact hx.1 + · by_contra H + exact hx.2 (h₁ H) + rw [Set.uIoc_of_le (le_of_lt h₀)] at t₂ + rw [Set.Ioc_diff_Ioo_same h₀] at t₂ + assumption + calc volume {a_1 | a_1 ∈ Ι a b ∧ f a_1 ≠ g a_1} + _ ≤ volume {b} := volume.mono this + _ = 0 := volume_singleton + 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 : ℝ} : x ∈ Set.Ioo 0 (π / 2) → log (sin (2 * x)) = log 2 + log (sin x) + log (cos x) := by + intro hx + simp at hx - 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 + -- sin x ≠ 0 + apply (fun a => Ne.symm (ne_of_lt a)) + apply sin_pos_of_mem_Ioo + constructor + · exact hx.1 + · linarith [pi_pos, hx.2] + -- 2 * sin x ≠ 0 + simp + apply (fun a => Ne.symm (ne_of_lt a)) + apply sin_pos_of_mem_Ioo + constructor + · exact hx.1 + · linarith [pi_pos, hx.2] + -- cos x ≠ 0 + apply (fun a => Ne.symm (ne_of_lt a)) + apply cos_pos_of_mem_Ioo + constructor + · linarith [pi_pos, hx.1] + · exact hx.2 - have t₂ {x : ℝ} : log (sin x) = log (sin (2 * x)) - log 2 - log (cos x) := by - rw [t₁] + have t₂ : Set.EqOn (fun y ↦ log (sin y)) (fun y ↦ log (sin (2 * y)) - log 2 - log (cos y)) (Set.Ioo 0 (π / 2)) := by + intro x hx + simp + rw [t₁ hx] ring - conv => - left - arg 1 - intro x - rw [t₂] - + rw [intervalIntegral.integral_congr_volume _ 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))] @@ -255,24 +298,57 @@ lemma integral_log_sin : ∫ (x : ℝ) in (0)..(π / 2), log (sin x) = -log 2 * rw [this] have : ∫ (x : ℝ) in (0)..π, log (sin x) = 2 * ∫ (x : ℝ) in (0)..(π / 2), log (sin x) := by - sorry + 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] + have : ∫ (x : ℝ) in (0)..(π / 2), log (sin x) = ∫ (x : ℝ) in (0)..(π / 2), log (cos x) := by - sorry + conv => + right + arg 1 + intro x + rw [← sin_pi_div_two_sub] + rw [intervalIntegral.integral_comp_sub_left (fun x ↦ log (sin x)) (π / 2)] + simp rw [← this] simp linarith exact Ne.symm (NeZero.ne' 2) -- IntervalIntegrable (fun x => log (sin (2 * x))) volume 0 (π / 2) - sorry + let A := intervalIntegrable_log_sin.comp_mul_left 2 + simp at A + assumption -- 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 + let A := intervalIntegrable_log_sin.comp_mul_left 2 + simp at A + assumption -- -- IntervalIntegrable (fun x => log 2) volume 0 (π / 2) simp -- -- IntervalIntegrable (fun x => log (cos x)) volume 0 (π / 2) exact intervalIntegrable_log_cos + -- + linarith [pi_pos]