Lean 4 Proof

private lemma quotient_rule_variance_eq (a b c : ℝ)
    (hc : c ≠ 0) :
    (a * c - b * b) / c ^ 2 =
      a / c - (b / c) ^ 2 := by
  field_simp

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/InformationGeometry.lean:777

Module Section

The VRI σ² = T·χ is fundamentally an exponential family identity:

In the same file