Documentation

Lean 4 Proof

theorem platform_cross_externality_positive {aB aS ρ : ℝ}
    (haB : 0 < aB) (haS : 0 < aS) (hρ : ρ < 1) (hρne : ρ ≠ 0)
    {nB nS : ℝ} (hnB : 0 < nB) (hnS : 0 < nS) :
    (1 - ρ) * aB * aS * nB ^ (ρ - 1) * nS ^ (ρ - 1) *
      (platformValue aB aS ρ nB nS) ^ (1 - 2 * ρ) > 0 :=
  cross_externality_positive haB haS hρ hρne hnB hnS

Dependency Graph

Location

thesis/CESProofs/EntryExit/NetworkEntry.lean:83

Module Section

Paper 1c, Section 6: Endogenous Network Scaling

In the same file