Documentation

Lean 4 Proof

theorem timescale_ratio_eq_rate_ratio {rSlow rFast : ℝ}
    (hSlow : 0 < rSlow) (hFast : 0 < rFast) :
    timescaleFromRate rSlow / timescaleFromRate rFast =
    spectralGapRatio rSlow rFast := by
  simp only [timescaleFromRate, spectralGapRatio]
  field_simp

Dependency Graph

Used by

Location

thesis/CESProofs/Hierarchy/SpectralHierarchy.lean:60

Module Section

Endogenous Hierarchy: Why N Levels?

In the same file