Documentation

Lean 4 Proof

theorem ceiling_bound {phi_prev sigma_n Fbar_n : ℝ}
    (hs : 0 < sigma_n)
    (hbound : Fbar_n * sigma_n ≤ phi_prev) :
    Fbar_n ≤ phi_prev / sigma_n := by
  rwa [le_div_iff₀ hs]

Dependency Graph

Location

thesis/CESProofs/Hierarchy/TransitionDynamics.lean:31

Module Section

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

In the same file