Compare commits

..

No commits in common. "eb58a8df04c82e9d163f61e0f614f224e6ce8c83" and "3063415cf995946a5122051d0549797b5907cb3e" have entirely different histories.

3 changed files with 110 additions and 127 deletions

View File

@ -1,62 +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
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,65 +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
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]

View File

@ -6,6 +6,7 @@ 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
@ -226,6 +227,62 @@ 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
@ -276,3 +333,56 @@ 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₁₁