Documentation

Lean 4 Proof

theorem decomposability_monotone {ε₁ ε₂ : ℝ}
    (h1 : 0 < ε₁) (_h2 : 0 < ε₂) (hlt : ε₁ < ε₂) :
    1 / ε₂ - 1 < 1 / ε₁ - 1 := by
  linarith [one_div_lt_one_div_of_lt h1 hlt]

Dependency Graph

Location

thesis/CESProofs/Hierarchy/SpectralHierarchy.lean:220

Module Section

Endogenous Hierarchy: Why N Levels?

In the same file