From b2de8dbc445f2feec8c91fcc2d0a3988273b36f9 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Wed, 14 Aug 2024 14:12:57 +0200 Subject: [PATCH] working --- Nevanlinna/specialFunctions_Integrals.lean | 178 ++++++++++++++++++--- 1 file changed, 159 insertions(+), 19 deletions(-) diff --git a/Nevanlinna/specialFunctions_Integrals.lean b/Nevanlinna/specialFunctions_Integrals.lean index 839e9e0..957bbb8 100644 --- a/Nevanlinna/specialFunctions_Integrals.lean +++ b/Nevanlinna/specialFunctions_Integrals.lean @@ -8,12 +8,142 @@ 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 + by_cases h'x : x = 0 + · rw [h'x]; simp + + -- 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 + have l₁ : 0 ≤ sin x := by + apply sin_nonneg_of_nonneg_of_le_pi (Set.mem_Icc.1 hx).1 + trans (1 : ℝ) + exact (Set.mem_Icc.1 hx).2 + trans π / 2 + exact one_le_pi_div_two + norm_num [pi_nonneg] + have l₂ : log (sin x) ≤ 0 := log_nonpos l₁ (sin_le_one x) + + simp only [norm_eq_abs, Function.comp_apply] + rw [abs_eq_neg_self.2 l₀] + rw [abs_eq_neg_self.2 l₂] + simp only [neg_le_neg_iff, ge_iff_le] + + have l₃ : x ∈ (Set.Ioi 0) := by + 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 + apply div_pos pi_pos zero_lt_two + exact l₃ + + have : ∀ x ∈ (Set.Icc 0 (π / 2)), (π / 2)⁻¹ * x ≤ sin x := by + intro x hx + + have i₀ : 0 ∈ Set.Icc 0 π := + Set.left_mem_Icc.mpr pi_nonneg + have i₁ : π / 2 ∈ Set.Icc 0 π := + Set.mem_Icc.mpr ⟨div_nonneg pi_nonneg zero_le_two, half_le_self pi_nonneg⟩ + + have i₂ : 0 ≤ 1 - (π / 2)⁻¹ * x := by + rw [sub_nonneg] + calc (π / 2)⁻¹ * x + _ ≤ (π / 2)⁻¹ * (π / 2) := by + apply mul_le_mul_of_nonneg_left + exact (Set.mem_Icc.1 hx).2 + apply inv_nonneg.mpr (div_nonneg pi_nonneg zero_le_two) + _ = 1 := by + apply inv_mul_cancel + apply div_ne_zero_iff.mpr + constructor + · exact pi_ne_zero + · exact Ne.symm (NeZero.ne' 2) + + have i₃ : 0 ≤ (π / 2)⁻¹ * x := by + apply mul_nonneg + apply inv_nonneg.2 + apply div_nonneg + exact pi_nonneg + exact zero_le_two + exact (Set.mem_Icc.1 hx).1 + + have i₄ : 1 - (π / 2)⁻¹ * x + (π / 2)⁻¹ * x = 1 := by ring + + let B := strictConcaveOn_sin_Icc.concaveOn.2 i₀ i₁ i₂ i₃ i₄ + simp [Real.sin_pi_div_two] at B + rw [(by ring_nf; rw [mul_inv_cancel pi_ne_zero, one_mul] : 2 / π * x * (π / 2) = x)] at B + simpa + + apply log_le_log l₅ + apply this + apply Set.mem_Icc.mpr + constructor + · exact le_of_lt l₃ + · trans 1 + exact (Set.mem_Icc.1 hx).2 + exact one_le_pi_div_two + + example : IntervalIntegrable (log ∘ sin) volume 0 1 := by - have int_log : IntervalIntegrable log volume 0 1 := by sorry + have int_log : IntervalIntegrable (fun x ↦ ‖log x‖) volume 0 1 := by + apply IntervalIntegrable.norm + rw [← neg_neg log] + apply IntervalIntegrable.neg + apply intervalIntegrable_deriv_of_nonneg (g := fun x ↦ -(x * log x - x)) + · exact (continuous_mul_log.continuousOn.sub continuous_id.continuousOn).neg + · intro x hx + norm_num at hx + convert ((hasDerivAt_mul_log hx.left.ne.symm).sub (hasDerivAt_id x)).neg using 1 + norm_num + · intro x hx + norm_num at hx + rw [Pi.neg_apply, Left.nonneg_neg_iff] + exact (log_nonpos_iff hx.left).mpr hx.right.le - apply IntervalIntegrable.mono_fun' (g := log) + have int_log : IntervalIntegrable (fun x ↦ ‖log ((π / 2)⁻¹ * x)‖) volume 0 1 := by + + have A := IntervalIntegrable.comp_mul_right int_log (π / 2)⁻¹ + simp only [norm_eq_abs] at A + conv => + arg 1 + intro x + rw [mul_comm] + simp only [norm_eq_abs] + apply IntervalIntegrable.mono A + simp + trans Set.Icc 0 (π / 2) + exact Set.Icc_subset_Icc (Preorder.le_refl 0) one_le_pi_div_two + exact Set.Icc_subset_uIcc + exact Preorder.le_refl volume + + apply IntervalIntegrable.mono_fun' (g := fun x ↦ ‖log ((π / 2)⁻¹ * x)‖) exact int_log -- AEStronglyMeasurable (log ∘ sin) (volume.restrict (Ι 0 1)) @@ -24,32 +154,42 @@ example : IntervalIntegrable (log ∘ sin) volume 0 1 := by intro x hx by_contra contra simp at contra - rw [contra] at hx - rw [Set.left_mem_uIoc] at hx + rw [contra, Set.left_mem_uIoc] at hx linarith exact continuousOn_sin - -- + + -- Set.MapsTo sin (Ι 0 1) (Ι 0 1) rw [Set.uIoc_of_le (zero_le_one' ℝ)] exact fun x hx ↦ ⟨sin_pos_of_pos_of_le_one hx.1 hx.2, sin_le_one x⟩ - -- - exact measurableSet_uIoc - -- - have : ∀ x ∈ (Ι 0 1), ‖(log ∘ sin) x‖ ≤ log x := by sorry + -- MeasurableSet (Ι 0 1) + exact measurableSet_uIoc + + -- (fun x => ‖(log ∘ sin) x‖) ≤ᶠ[ae (volume.restrict (Ι 0 1))] ‖log‖ dsimp [EventuallyLE] rw [MeasureTheory.ae_restrict_iff] apply MeasureTheory.ae_of_all - exact this + intro x hx + have : x ∈ Set.Icc 0 1 := by + simp + simp at hx + constructor + · exact le_of_lt hx.1 + · exact hx.2 + let A := logsinBound x this + simp only [Function.comp_apply, norm_eq_abs] at A + exact A - --intro x - rw [MeasureTheory.ae_iff] - simp - - rw [MeasureTheory.ae_iff] - simp - - - sorry + apply measurableSet_le + apply Measurable.comp' + exact continuous_abs.measurable + exact Measurable.comp' measurable_log continuous_sin.measurable + -- Measurable fun a => |log ((π / 2)⁻¹ * a)| + apply Measurable.comp' + exact continuous_abs.measurable + apply Measurable.comp' + exact measurable_log + exact measurable_const_mul (π / 2)⁻¹ theorem logInt