pith. machine review for the scientific record. sign in
def definition def or abbrev

wealthDistributionCert

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  51noncomputable def wealthDistributionCert : WealthDistributionCert where
  52  exponent_eq_phi := paretoExponent_eq_phi

proof body

Definition body.

  53  exponent_band := paretoExponent_band
  54  inv_phi := inv_phi_eq
  55
  56end IndisputableMonolith.Economics.WealthDistributionFromSigma

depends on (4)

Lean names referenced from this declaration's body.