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
22 results
(filtered from 2160)
Fiedler Vector
noncomputable def
proved
Hierarchy
thesis/CESProofs/CurvatureRoles/NetworkCES.lean
:118
Sector Herfindahl
noncomputable def
proved
Dynamics & Crises
thesis/CESProofs/Dynamics/Defs.lean
:238
Sector General Curvature
noncomputable def
proved
Dynamics & Crises
thesis/CESProofs/Dynamics/Defs.lean
:242
Sector General Effective Curvature
noncomputable def
proved
Dynamics & Crises
thesis/CESProofs/Dynamics/Defs.lean
:247
Herfindahl Adjusted Rho
noncomputable def
proved
Dynamics & Crises
thesis/CESProofs/Dynamics/Defs.lean
:255
Critical Knockout Weight
noncomputable def
proved
Dynamics & Crises
thesis/CESProofs/Dynamics/Defs.lean
:260
Mode Rate
noncomputable def
proved
Foundations
thesis/CESProofs/Foundations/Emergence.lean
:119
Mode After L
noncomputable def
proved
Foundations
thesis/CESProofs/Foundations/Emergence.lean
:125
Level Herfindahl
noncomputable def
proved
Hierarchy
thesis/CESProofs/Hierarchy/Defs.lean
:314
Level General Curvature
noncomputable def
proved
Hierarchy
thesis/CESProofs/Hierarchy/Defs.lean
:318
Level Standard Curvature
noncomputable def
proved
Hierarchy
thesis/CESProofs/Hierarchy/Defs.lean
:322
Weighted NGM Entry
noncomputable def
proved
Hierarchy
thesis/CESProofs/Hierarchy/Defs.lean
:328
Weighted Cycle Product Beta
noncomputable def
proved
Hierarchy
thesis/CESProofs/Hierarchy/Defs.lean
:333
Is Critical Supplier
noncomputable def
proved
Hierarchy
thesis/CESProofs/Hierarchy/Defs.lean
:338
Count Critical Suppliers
noncomputable def
proved
Hierarchy
thesis/CESProofs/Hierarchy/Defs.lean
:344
General Effective Curvature Keff
noncomputable def
proved
CES Potential
thesis/CESProofs/Potential/EffectiveCurvature.lean
:247
General Critical Friction
noncomputable def
proved
CES Potential
thesis/CESProofs/Potential/EffectiveCurvature.lean
:253
IRS Effective Curvature Perp
noncomputable def
proved
CES Potential
thesis/CESProofs/Potential/EffectiveCurvature.lean
:260
IRS Critical Friction Perp
noncomputable def
proved
CES Potential
thesis/CESProofs/Potential/EffectiveCurvature.lean
:266
Weighted Knockout Loss
noncomputable def
proved
CES Potential
thesis/CESProofs/Potential/EffectiveCurvature.lean
:273
Expected Knockout Loss
noncomputable def
proved
CES Potential
thesis/CESProofs/Potential/EffectiveCurvature.lean
:280
IRS Firm Profit
noncomputable def
proved
CES Potential
thesis/CESProofs/Potential/EffectiveCurvature.lean
:287