ces
Claw
Papers
Wiki
Theorems
Tests
Forum
Skills
Settings
Sign in
All Lean 4 Declarations
2160 declarations
Back to section overview
All kinds
axiom
def
inductive
lemma
noncomputable def
structure
theorem
All categories
Foundations
Curvature Roles
Info Geometry
CES Potential
Dynamics & Crises
Hierarchy
Trade
AI Transition
Monetary Policy
Empirical Methods
Microeconomics
Macroeconomics
All statuses
proved
sorry
axiom
trivial
Clear
29 results
(filtered from 2160)
cesPriceIndex_pos
theorem
proved
applications
thesis/CESProofs/Applications/Economics.lean
:1013
cesIndirectUtility
def
proved
applications
thesis/CESProofs/Applications/Economics.lean
:1027
cesExpenditureFunction
def
proved
applications
thesis/CESProofs/Applications/Economics.lean
:1035
expenditure_indirect_duality
theorem
proved
applications
thesis/CESProofs/Applications/Economics.lean
:1043
indirect_utility_antitone_in_price
theorem
proved
applications
thesis/CESProofs/Applications/Economics.lean
:1056
roys_identity_ratio
theorem
proved
applications
thesis/CESProofs/Applications/Economics.lean
:1081
foundationGrowthFactor
def
proved
applications
thesis/CESProofs/Applications/FairInheritance.lean
:472
foundationShareGrowth
def
proved
applications
thesis/CESProofs/Applications/FairInheritance.lean
:481
indexedPayoutRate
def
proved
applications
thesis/CESProofs/Applications/FairInheritance.lean
:487
foundation_accumulates
theorem
proved
applications
thesis/CESProofs/Applications/FairInheritance.lean
:497
foundation_share_grows
theorem
proved
applications
thesis/CESProofs/Applications/FairInheritance.lean
:509
fixed_payout_fails
theorem
proved
applications
thesis/CESProofs/Applications/FairInheritance.lean
:526
indexed_payout_bounds_growth
theorem
proved
applications
thesis/CESProofs/Applications/FairInheritance.lean
:547
foundation_tax_savings
theorem
proved
applications
thesis/CESProofs/Applications/FairInheritance.lean
:567
foundation_nonrecognition_closes
theorem
proved
applications
thesis/CESProofs/Applications/FairInheritance.lean
:584
realBenchmark
def
proved
applications
thesis/CESProofs/Applications/FairInheritance.lean
:609
smoothPayout
def
proved
applications
thesis/CESProofs/Applications/FairInheritance.lean
:613
smoothRetained
def
proved
applications
thesis/CESProofs/Applications/FairInheritance.lean
:617
smooth_payout_nonneg
theorem
proved
applications
thesis/CESProofs/Applications/FairInheritance.lean
:621
inflation_erodes_foundation
theorem
proved
applications
thesis/CESProofs/Applications/FairInheritance.lean
:632
smooth_rebuild
theorem
proved
applications
thesis/CESProofs/Applications/FairInheritance.lean
:643
smooth_payout_bounded
theorem
proved
applications
thesis/CESProofs/Applications/FairInheritance.lean
:651
smooth_retained_above
theorem
proved
applications
thesis/CESProofs/Applications/FairInheritance.lean
:661
excess_contraction_factor
theorem
proved
applications
thesis/CESProofs/Applications/FairInheritance.lean
:673
smooth_dominates_fixed
theorem
proved
applications
thesis/CESProofs/Applications/FairInheritance.lean
:684
foundation_transfer_cap_integrity
theorem
proved
applications
thesis/CESProofs/Applications/FairInheritance.lean
:707
transfer_preserves_total_excess
theorem
proved
applications
thesis/CESProofs/Applications/FairInheritance.lean
:726
foundation_sourced_zero_cap
theorem
proved
applications
thesis/CESProofs/Applications/FairInheritance.lean
:745
spinoff_gains_nothing
theorem
proved
applications
thesis/CESProofs/Applications/FairInheritance.lean
:759