Documentation

Lean 4 Proof

theorem higher_J_raises_value {J₁ J₂ ρ c : ℝ}
    (hJ₁ : 1 < J₁) (hJ₁₂ : J₁ < J₂) (hρ0 : 0 < ρ) (hρ1 : ρ < 1) (hc : 0 < c) :
    valueFunction J₁ ρ c < valueFunction J₂ ρ c :=
  valueFunction_increasing hJ₁ hJ₁₂ hρ0 hρ1 hc

Dependency Graph

Location

thesis/CESProofs/Dynamics/HierarchicalJ.lean:138

Module Section

Paper 3c, Section 6: Hierarchical Implications

In the same file