Documentation

Lean 4 Proof

def crossBlockCoupling (baseCoupling c c₀ : ℝ) : ℝ :=
  baseCoupling * Real.exp (-c / c₀)

Dependency Graph

Used by

Location

thesis/CESProofs/Hierarchy/SpectralHierarchy.lean:235

Module Section

Endogenous Hierarchy: Why N Levels?

In the same file