Documentation

Lean 4 Proof

theorem bridgeRatio_pos {ρ : ℝ} (hρ0 : 0 < ρ) (hρ1 : ρ < 1) :
    0 < bridgeRatio ρ := by
  simp only [bridgeRatio]
  apply div_pos
  · linarith
  · positivity

Dependency Graph

Location

thesis/CESProofs/Foundations/InformationGeometry.lean:367

Module Section

Information Geometry of CES:

In the same file