Documentation

Lean 4 Proof

def geometricMeanPeriod (tau_n tau_m : ℝ) : ℝ :=
  2 * Real.pi * Real.sqrt (tau_n * tau_m)

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/BusinessCycles.lean:102

Module Section

Results 47-62: Business Cycles on the CES Landscape

In the same file