Documentation

Lean 4 Proof

theorem linear_at_zero (s0j s1j : ℝ) :
    linearShareComponent s0j s1j 0 = s0j := by
  simp [linearShareComponent]

Dependency Graph

Location

thesis/CESProofs/Foundations/InformationGeometry.lean:545

Module Section

Information Geometry of CES:

In the same file