Documentation

Lean 4 Proof

def cesCapitalShare (α r_KL ρ : ℝ) : ℝ :=
  α * r_KL ^ ρ / (α * r_KL ^ ρ + (1 - α))

Dependency Graph

Location

thesis/CESProofs/Applications/FairInheritance.lean:81

Module Section

Fair Inheritance: Taxing Concentration, Not Transfer

In the same file