Splitting off files

This commit is contained in:
Stefan Kebekus 2024-08-15 08:27:00 +02:00
parent c124cccb01
commit eb58a8df04
4 changed files with 0 additions and 1090 deletions

View File

@ -8,275 +8,6 @@ open Real Filter MeasureTheory intervalIntegral
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
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 : )
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₅ : 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
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
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)⁻¹
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]
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 lemma int₁₁ : ∫ (x : ) in (0)..π, log (4 * sin x ^ 2) = 0 := by
sorry sorry

View File

@ -9,224 +9,6 @@ open Real Filter MeasureTheory intervalIntegral
-- The following theorem was suggested by Gareth Ma on Zulip -- 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
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 : )
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₅ : 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
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
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)⁻¹
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 theorem logInt
{t : } {t : }
(ht : 0 < t) : (ht : 0 < t) :
@ -281,108 +63,3 @@ theorem logInt
exact (log_nonpos_iff hx.left).mpr hx.right.le exact (log_nonpos_iff hx.left).mpr hx.right.le
· -- log is integrable on [[0, t]] · -- log is integrable on [[0, t]]
simp [Set.mem_uIcc, ht] simp [Set.mem_uIcc, ht]
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
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₁₁

View File

@ -6,7 +6,6 @@ import Mathlib.MeasureTheory.Measure.Restrict
open scoped Interval Topology open scoped Interval Topology
open Real Filter MeasureTheory intervalIntegral 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 lemma logsinBound : ∀ x ∈ (Set.Icc 0 1), ‖(log ∘ sin) x‖ ≤ ‖log ((π / 2)⁻¹ * x)‖ := by
@ -227,62 +226,6 @@ lemma intervalIntegrable_log_cos : IntervalIntegrable (log ∘ cos) volume 0 (π
rwa [← this] rwa [← this]
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 integral_log_sin : ∫ (x : ) in (0)..(π / 2), log (sin x) = -log 2 * π/2 := 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 : } : sin (2 * x) = 2 * sin x * cos x := sin_two_mul x
@ -333,56 +276,3 @@ lemma integral_log_sin : ∫ (x : ) in (0)..(π / 2), log (sin x) = -log 2 *
simp simp
-- -- IntervalIntegrable (fun x => log (cos x)) volume 0 (π / 2) -- -- IntervalIntegrable (fun x => log (cos x)) volume 0 (π / 2)
exact intervalIntegrable_log_cos exact intervalIntegrable_log_cos
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₁₁

View File

@ -1,388 +0,0 @@
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
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 : )
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₅ : 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
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
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)⁻¹
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 : }
(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 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
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₁₁