Documentation

Lean 4 Proof

def totalRevenue (R_ad R_mp φ : ℝ) : ℝ :=
  (1 - φ) * R_ad + φ * R_mp

Dependency Graph

Used by

Location

thesis/CESProofs/Applications/KnowledgeCommons.lean:100

Module Section

Paper 10: The Knowledge Commons Paradox:

In the same file