Documentation

Lean 4 Proof

theorem cesPotential_zero_friction (q : ℝ) (p ε : Fin J → ℝ) :
    cesPotential J q 0 p ε = ∑ j : Fin J, p j * ε j := by
  simp [cesPotential]

Dependency Graph

Location

thesis/CESProofs/Potential/CESPotential.lean:99

Module Section

Theorem 3: CES Potential Uniqueness (Paper 2, Section 3.2)

In the same file