Documentation

Lean 4 Proof

theorem larger_J_larger_network {J₁ J₂ : ℝ} {ρ c : ℝ}
    (hJ₁ : 0 < J₁) (hJ₁₂ : J₁ < J₂) (hρ : 0 < ρ) (hc : 0 < c) :
    J₁ ^ (1 / ρ) * c < J₂ ^ (1 / ρ) * c := by
  apply mul_lt_mul_of_pos_right _ hc
  exact rpow_lt_rpow (le_of_lt hJ₁) hJ₁₂ (div_pos one_pos hρ)

Dependency Graph

Location

thesis/CESProofs/EntryExit/NetworkEntry.lean:39

Module Section

Paper 1c, Section 6: Endogenous Network Scaling

In the same file