Documentation

Lean 4 Proof

def outerCES (α Q C ρ_outer : ℝ) : ℝ :=
  (α * Q ^ ρ_outer + (1 - α) * C ^ ρ_outer) ^ (1 / ρ_outer)

Dependency Graph

Location

thesis/CESProofs/Applications/KnowledgeCommons.lean:328

Module Section

Paper 10: The Knowledge Commons Paradox:

In the same file