Documentation

Lean 4 Proof

theorem no_shock_linear_trivial (s0j : ℝ) (t : ℝ) :
    linearShareComponent s0j s0j t = s0j := by
  simp only [linearShareComponent]; ring

Dependency Graph

Location

thesis/CESProofs/Foundations/InformationGeometry.lean:641

Module Section

Information Geometry of CES:

In the same file