Documentation

Lean 4 Proof

theorem cross_externality_positive {aB aS ρ : ℝ}
    (haB : 0 < aB) (haS : 0 < aS)
    (hρ : ρ < 1) (_hρne : ρ ≠ 0)
    {nB nS : ℝ} (hnB : 0 < nB) (hnS : 0 < nS) :
    -- ∂²V/∂n_B∂n_S = (1-ρ)·a_B·a_S·n_B^{ρ-1}·n_S^{ρ-1}·V^{1-2ρ} > 0
    (1 - ρ) * aB * aS * nB ^ (ρ - 1) * nS ^ (ρ - 1) *
      (platformValue aB aS ρ nB nS) ^ (1 - 2 * ρ) > 0 := by
  apply mul_pos
  · apply mul_pos
    · apply mul_pos
      · apply mul_pos
        · apply mul_pos
          · linarith
          · exact haB
        · exact haS
      · exact rpow_pos_of_pos hnB _
    · exact rpow_pos_of_pos hnS _
  · apply rpow_pos_of_pos
    simp only [platformValue]
    apply rpow_pos_of_pos
    apply add_pos
    · exact mul_pos haB (rpow_pos_of_pos hnB _)
    · exact mul_pos haS (rpow_pos_of_pos hnS _)

Dependency Graph

Used by

Location

thesis/CESProofs/CurvatureRoles/NetworkCES.lean:756

Module Section

## Network Scaling Results

In the same file