Update specialFunctions_Integrals.lean
This commit is contained in:
Stefan Kebekus
parent
b2de8dbc44
commit
3063415cf9
|
|
@ -9,7 +9,6 @@ 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
|
||||
|
|
@ -18,8 +17,21 @@ lemma logsinBound : ∀ x ∈ (Set.Icc 0 1), ‖(log ∘ sin) x‖ ≤ ‖log ((
|
|||
|
||||
-- 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
|
||||
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 : ℝ)
|
||||
|
|
@ -38,24 +50,6 @@ lemma logsinBound : ∀ x ∈ (Set.Icc 0 1), ‖(log ∘ sin) x‖ ≤ ‖log ((
|
|||
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
|
||||
|
|
@ -109,7 +103,7 @@ lemma logsinBound : ∀ x ∈ (Set.Icc 0 1), ‖(log ∘ sin) x‖ ≤ ‖log ((
|
|||
exact one_le_pi_div_two
|
||||
|
||||
|
||||
example : IntervalIntegrable (log ∘ sin) volume 0 1 := by
|
||||
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
|
||||
|
|
@ -191,6 +185,47 @@ example : IntervalIntegrable (log ∘ sin) volume 0 1 := by
|
|||
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 : ℝ}
|
||||
|
|
@ -248,8 +283,59 @@ theorem logInt
|
|||
simp [Set.mem_uIcc, ht]
|
||||
|
||||
|
||||
lemma int₁₁ : ∫ (x : ℝ) in (0)..π, log (4 * sin x ^ 2) = 0 := 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 : ℝ} : 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
|
||||
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue