Documentation

Lean 4 Proof

theorem total_spread_eq_endpoint_ratio (spec : OrderedSpectrum M)
    (hM : 1 < M) :
    spec.rate ⟨0, by omega⟩ / spec.rate ⟨M - 1, by omega⟩ =
    timescaleFromRate (spec.rate ⟨M - 1, by omega⟩) /
      timescaleFromRate (spec.rate ⟨0, by omega⟩) := by
  simp only [timescaleFromRate]
  field_simp

Dependency Graph

Location

thesis/CESProofs/Hierarchy/SpectralHierarchy.lean:113

Module Section

Endogenous Hierarchy: Why N Levels?

In the same file