integral_cot_from_theta

proof body

Tactic-mode proof.

  50  -- Standard calculus result: ∫ cot θ dθ = log(sin θ) + C.
  51  -- We prove it via FTC on `f(θ) = log(sin θ)` over `[θ_s, π/2]`.
  52  let f : ℝ → ℝ := fun θ => Real.log (Real.sin θ)
  53
  54  have hpi2ltpi : (Real.pi / 2 : ℝ) < Real.pi := by nlinarith [Real.pi_pos]
  55
  56  have hsin_ne0_uIcc : ∀ x ∈ Set.uIcc θ_s (π/2), Real.sin x ≠ 0 := by
  57    intro x hx
  58    have hx' : θ_s ≤ x ∧ x ≤ π/2 := by
  59      rcases Set.mem_uIcc.mp hx with hx' | hx'
  60      · exact hx'
  61      · exfalso
  62        have : (π/2 : ℝ) ≤ θ_s := le_trans hx'.1 hx'.2
  63        exact (not_le_of_lt hθ.2) this
  64    have hxpos : 0 < x := lt_of_lt_of_le hθ.1 hx'.1
  65    have hxltpi : x < Real.pi := lt_of_le_of_lt hx'.2 hpi2ltpi
  66    exact ne_of_gt (Real.sin_pos_of_pos_of_lt_pi hxpos hxltpi)
  67
  68  have hderiv_eq_cot_uIoc : Set.EqOn (fun x => deriv f x) (fun x => Real.cot x) (Set.uIoc θ_s (π/2)) := by
  69    intro x hx
  70    have hx' : θ_s < x ∧ x ≤ π/2 := by
  71      rcases Set.mem_uIoc.mp hx with hx' | hx'
  72      · exact hx'
  73      · exfalso
  74        have : (π/2 : ℝ) ≤ θ_s := le_trans (le_of_lt hx'.1) hx'.2
  75        exact (not_le_of_lt hθ.2) this
  76    have hxpos : 0 < x := lt_of_lt_of_le hθ.1 (le_of_lt hx'.1)
  77    have hxltpi : x < Real.pi := lt_of_le_of_lt hx'.2 hpi2ltpi
  78    have hsx : Real.sin x ≠ 0 := ne_of_gt (Real.sin_pos_of_pos_of_lt_pi hxpos hxltpi)
  79    have hlog : HasDerivAt Real.log (Real.sin x)⁻¹ (Real.sin x) := Real.hasDerivAt_log hsx
  80    have hsin : HasDerivAt Real.sin (Real.cos x) x := Real.hasDerivAt_sin x
  81    have hcomp :
  82        HasDerivAt (fun t => Real.log (Real.sin t)) ((Real.sin x)⁻¹ * Real.cos x) x :=
  83      (HasDerivAt.comp x hlog hsin)
  84    -- Turn the computed derivative into `deriv f x = cot x`.
  85    have hderiv : deriv (fun t => Real.log (Real.sin t)) x = (Real.sin x)⁻¹ * Real.cos x := hcomp.deriv
  86    have hmul_to_div : (Real.sin x)⁻¹ * Real.cos x = Real.cos x / Real.sin x := by
  87      simp [div_eq_mul_inv, mul_comm, mul_left_comm, mul_assoc]
  88    calc
  89      deriv f x = (Real.sin x)⁻¹ * Real.cos x := by simpa [f] using hderiv
  90      _ = Real.cos x / Real.sin x := hmul_to_div
  91      _ = Real.cot x := by simpa using (Real.cot_eq_cos_div_sin x).symm
  92
  93  have hdiff : ∀ x ∈ Set.uIcc θ_s (π/2), DifferentiableAt ℝ f x := by
  94    intro x hx
  95    have hsx : Real.sin x ≠ 0 := hsin_ne0_uIcc x hx
  96    have hlog : HasDerivAt Real.log (Real.sin x)⁻¹ (Real.sin x) := Real.hasDerivAt_log hsx
  97    have hsin : HasDerivAt Real.sin (Real.cos x) x := Real.hasDerivAt_sin x
  98    have hcomp : HasDerivAt (fun t => Real.log (Real.sin t)) ((Real.sin x)⁻¹ * Real.cos x) x :=
  99      (HasDerivAt.comp x hlog hsin)
 100    -- `f` is definitionally the same function.
 101    simpa [f] using hcomp.differentiableAt
 102
 103  have hCotCont : ContinuousOn (fun x => Real.cot x) (Set.uIcc θ_s (π/2)) := by
 104    -- On `[θ_s, π/2]` we have `sin x ≠ 0`, so `cot x = cos x / sin x` is continuous.
 105    have hcos : ContinuousOn Real.cos (Set.uIcc θ_s (π/2)) :=
 106      (Real.continuous_cos.continuousOn)
 107    have hsin : ContinuousOn Real.sin (Set.uIcc θ_s (π/2)) :=
 108      (Real.continuous_sin.continuousOn)
 109    have hsin_ne0 : ∀ x ∈ Set.uIcc θ_s (π/2), Real.sin x ≠ 0 := hsin_ne0_uIcc
 110    have hdiv : ContinuousOn (fun x => Real.cos x / Real.sin x) (Set.uIcc θ_s (π/2)) :=
 111      (hcos.div hsin hsin_ne0)
 112    simpa [Real.cot_eq_cos_div_sin] using hdiv
 113
 114  have hCotInt : IntervalIntegrable (fun x => Real.cot x) MeasureTheory.volume θ_s (π/2) :=
 115    hCotCont.intervalIntegrable
 116
 117  have hDerivInt : IntervalIntegrable (fun x => deriv f x) MeasureTheory.volume θ_s (π/2) := by
 118    have hEq : Set.EqOn (fun x => Real.cot x) (fun x => deriv f x) (Set.uIoc θ_s (π/2)) := by
 119      intro x hx
 120      simpa using (hderiv_eq_cot_uIoc hx).symm
 121    exact (IntervalIntegrable.congr hEq) hCotInt
 122
 123  have hFTC :
 124      ∫ x in θ_s..(π/2), deriv f x = f (π/2) - f θ_s :=
 125    intervalIntegral.integral_deriv_eq_sub (a := θ_s) (b := (π/2)) hdiff hDerivInt
 126
 127  have hcongr :
 128      (∫ x in θ_s..(π/2), Real.cot x) = (∫ x in θ_s..(π/2), deriv f x) := by
 129    have h_ae :
 130-- ... 23 more lines elided ...