Documentation

Lean 4 Proof

theorem diversity_premium_proportional_to_K_logJ (hJ : 2 ≤ J)
    {ρ : ℝ} (hρ : ρ ≠ 0) {c : ℝ} (hc : 0 < c) :
    Real.log (unnormCES J ρ (symmetricPoint J c) / c) - Real.log ↑J =
      (1 - ρ) / ρ * Real.log ↑J := by
  rw [network_log_premium (by omega) hρ hc]
  field_simp

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/NetworkCES.lean:865

Module Section

## Network Scaling Results

In the same file