Documentation

Lean 4 Proof

def alphaOfSigma (σ : ℝ) : ℝ := 1 - 2 / σ

Dependency Graph

Location

thesis/CESProofs/Foundations/TripleCorrespondence.lean:82

Module Section

### The Boltzmann-Escort Identification

In the same file