import Mathlib.Analysis.SpecialFunctions.Integrals import Mathlib.Analysis.SpecialFunctions.Log.NegMulLog import Mathlib.MeasureTheory.Integral.CircleIntegral import Mathlib.MeasureTheory.Measure.Restrict open scoped Interval Topology 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 (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 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)) apply ContinuousOn.aestronglyMeasurable apply ContinuousOn.comp (t := Ι 0 1) apply ContinuousOn.mono (s := {0}ᶜ) exact continuousOn_log intro x hx by_contra contra simp at contra 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⟩ -- 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 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 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 {t : ℝ} (ht : 0 < t) : ∫ x in (0 : ℝ)..t, log x = t * log t - t := by rw [← integral_add_adjacent_intervals (b := 1)] trans (-1) + (t * log t - t + 1) · congr · -- ∫ x in 0..1, log x = -1, same proof as before rw [integral_eq_sub_of_hasDerivAt_of_tendsto (f := fun x ↦ x * log x - x) (fa := 0) (fb := -1)] · simp · simp · intro x hx norm_num at hx convert (hasDerivAt_mul_log hx.left.ne.symm).sub (hasDerivAt_id x) using 1 norm_num · 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 · have := tendsto_log_mul_rpow_nhds_zero zero_lt_one simp_rw [rpow_one, mul_comm] at this -- tendsto_nhdsWithin_of_tendsto_nhds should be under Tendsto namespace convert this.sub (tendsto_nhdsWithin_of_tendsto_nhds tendsto_id) norm_num · rw [(by simp : -1 = 1 * log 1 - 1)] apply tendsto_nhdsWithin_of_tendsto_nhds exact (continuousAt_id.mul (continuousAt_log one_ne_zero)).sub continuousAt_id · -- ∫ x in 1..t, log x = t * log t + 1, just use integral_log_of_pos rw [integral_log_of_pos zero_lt_one ht] norm_num · abel · -- log is integrable on [[0, 1]] 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 · -- log is integrable on [[0, t]] simp [Set.mem_uIcc, ht] lemma int₁₁ : ∫ (x : ℝ) in (0)..π, log (4 * sin x ^ 2) = 0 := by sorry lemma int₁ : ∫ x in (0)..(2 * π), log ‖circleMap 0 1 x - 1‖ = 0 := by have {x : ℝ} : log ‖circleMap 0 1 x - 1‖ = log (4 * sin (x / 2) ^ 2) / 2 := by dsimp [Complex.abs] rw [log_sqrt (Complex.normSq_nonneg (circleMap 0 1 x - 1))] congr calc Complex.normSq (circleMap 0 1 x - 1) _ = (cos x - 1) * (cos x - 1) + sin x * sin x := by dsimp [circleMap] rw [Complex.normSq_apply] simp _ = sin x ^ 2 + cos x ^ 2 + 1 - 2 * cos x := by ring _ = 2 - 2 * cos x := by rw [sin_sq_add_cos_sq] norm_num _ = 2 - 2 * cos (2 * (x / 2)) := by rw [← mul_div_assoc] congr; norm_num _ = 4 - 4 * Real.cos (x / 2) ^ 2 := by rw [cos_two_mul] ring _ = 4 * sin (x / 2) ^ 2 := by nth_rw 1 [← mul_one 4, ← sin_sq_add_cos_sq (x / 2)] ring simp_rw [this] simp have : ∫ (x : ℝ) in (0)..2 * π, log (4 * sin (x / 2) ^ 2) = 2 * ∫ (x : ℝ) in (0)..π, log (4 * sin x ^ 2) := by have : 1 = 2 * (2 : ℝ)⁻¹ := by exact Eq.symm (mul_inv_cancel_of_invertible 2) nth_rw 1 [← one_mul (∫ (x : ℝ) in (0)..2 * π, log (4 * sin (x / 2) ^ 2))] rw [← mul_inv_cancel_of_invertible 2, mul_assoc] let f := fun y ↦ log (4 * sin y ^ 2) have {x : ℝ} : log (4 * sin (x / 2) ^ 2) = f (x / 2) := by simp conv => left right right arg 1 intro x rw [this] rw [intervalIntegral.inv_mul_integral_comp_div 2] simp rw [this] simp exact int₁₁