integral_cot_from_theta

formal source

  45      simpa [add_comm, add_left_comm, add_assoc, sub_eq_add_neg] using this
  46
  47/-- The integral of tan from θ_s to π/2 equals -ln(sin θ_s) -/
  48theorem integral_cot_from_theta (θ_s : ℝ) (hθ : 0 < θ_s ∧ θ_s < π/2) :
  49  ∫ θ in θ_s..(π/2), Real.cot θ = - Real.log (Real.sin θ_s) := by
  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)