Documentation

Lean 4 Proof

theorem curvature_dependence_ceiling {phi_prev sigma K1 K2 : ℝ}
    (hphi : 0 < phi_prev) (hs : 0 < sigma)
    (hK : K1 < K2) :
    -- Higher curvature means the gain function is more concave
    -- At the same input level, more complementary sectors have lower ceilings
    -- We state: (1 - K2) * phi / sigma < (1 - K1) * phi / sigma
    (1 - K2) * phi_prev / sigma < (1 - K1) * phi_prev / sigma := by
  apply div_lt_div_of_pos_right _ hs
  apply mul_lt_mul_of_pos_right _ hphi
  linarith

Dependency Graph

Location

thesis/CESProofs/Hierarchy/TransitionDynamics.lean:89

Module Section

Propositions 8-11, Theorems 10-12: Transition Dynamics

In the same file