Documentation

Lean 4 Proof

theorem premium_factor_eq_K_scaled (hJ : 2 ≤ J) {ρ : ℝ} (hρ : ρ ≠ 0) :
    (1 - ρ) / ρ = curvatureK J ρ * ↑J / ((↑J - 1) * ρ) := by
  simp only [curvatureK]
  have hJne : (↑J : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (by omega)
  have hJm1_ne : (↑J : ℝ) - 1 ≠ 0 := by
    have : (1 : ℝ) < ↑J := by exact_mod_cast (by omega : 1 < J)
    linarith
  field_simp

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/NetworkCES.lean:851

Module Section

## Network Scaling Results

In the same file