Documentation

Lean 4 Proof

theorem discriminating_prediction_at_midpoint (s0j s1j : ℝ) :
    linearShareComponent s0j s1j (1/2) = (s0j + s1j) / 2 := by
  simp only [linearShareComponent]; ring

Dependency Graph

Location

thesis/CESProofs/Foundations/InformationGeometry.lean:629

Module Section

Information Geometry of CES:

In the same file