Documentation

Lean 4 Proof

theorem spectralGap_pos {J : ℕ} (hJ : 2 ≤ J) {rho : ℝ} (hrho : rho < 1)
    {c : ℝ} (hc : 0 < c) :
    0 < (2 - rho) / (↑J * c) := by
  apply div_pos
  · linarith
  · exact mul_pos (Nat.cast_pos.mpr (by omega)) hc

Dependency Graph

Location

thesis/CESProofs/Hierarchy/Topology.lean:91

Module Section

Theorem 2, Propositions 1 and 4: CES-Forced Topology

In the same file