Documentation

Lean 4 Proof

theorem large_gap_implies_separation {rSlow rFast γ : ℝ}
    (hSlow : 0 < rSlow) (hFast : 0 < rFast) (_hγ : 0 < γ)
    (hgap : γ < spectralGapRatio rSlow rFast) :
    γ < timescaleFromRate rSlow / timescaleFromRate rFast := by
  rwa [timescale_ratio_eq_rate_ratio hSlow hFast]

Dependency Graph

Location

thesis/CESProofs/Hierarchy/SpectralHierarchy.lean:74

Module Section

Endogenous Hierarchy: Why N Levels?

In the same file