Documentation

Lean 4 Proof

theorem logRatio_antisymmetric {x : Fin J → ℝ}
    {j k : Fin J} (hj : 0 < x j) (hk : 0 < x k) :
    logRatio x j k = -logRatio x k j := by
  simp only [logRatio]
  rw [Real.log_div (ne_of_gt hj) (ne_of_gt hk),
      Real.log_div (ne_of_gt hk) (ne_of_gt hj)]
  ring

Dependency Graph

Location

thesis/CESProofs/Foundations/CESEstimation.lean:167

Module Section

CES Estimation Theory: Connecting Theory to Data

In the same file