Documentation

Lean 4 Proof

theorem slerp_weight_exceeds_half {θ : ℝ}
    (_hθ_pos : 0 < θ) (_hθ_lt : θ < Real.pi)
    (hcos : 0 < Real.cos (θ / 2)) (hcos_lt : Real.cos (θ / 2) < 1) :
    (1 : ℝ) / 2 < 1 / (2 * Real.cos (θ / 2)) := by
  have h2cos : 0 < 2 * Real.cos (θ / 2) := by positivity
  rw [div_lt_div_iff₀ (by norm_num : (0:ℝ) < 2) h2cos]
  nlinarith

Dependency Graph

Location

thesis/CESProofs/Foundations/InformationGeometry.lean:667

Module Section

Information Geometry of CES:

In the same file