Documentation

Lean 4 Proof

theorem ces_prudence_with_friction (J : ℕ) (ρ T Tstar c : ℝ) (hρ : ρ < 1)
    (hT : 0 ≤ T) (hTs : 0 < Tstar) (hc : 0 < c) :
    -- Effective prudence degrades linearly with friction
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Potential/EffectiveCurvature.lean:185

Module Section

Theorem 4 and Propositions 5-7, Corollary 1:

In the same file