Documentation

Lean 4 Proof

theorem network_scaling_at_equilibrium {J : ℕ} (hJ : 0 < J)
    {ρ : ℝ} (hρ : ρ ≠ 0) {c : ℝ} (hc : 0 < c) :
    unnormCES J ρ (symmetricPoint J c) = (↑J : ℝ) ^ (1 / ρ) * c :=
  network_scaling hJ hρ hc

Dependency Graph

Location

thesis/CESProofs/EntryExit/NetworkEntry.lean:32

Module Section

Paper 1c, Section 6: Endogenous Network Scaling

In the same file