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
23 results
(filtered from 2160)
Fr Inner Nonneg
lemma
proved
Curvature Roles
thesis/CESProofs/Applications/SettlementFeedback.lean
:349
Fr Below Critical
lemma
proved
Curvature Roles
thesis/CESProofs/Applications/SettlementFeedback.lean
:375
Continuous Min Div
lemma
proved
Curvature Roles
thesis/CESProofs/Applications/SettlementFeedback.lean
:403
Tendsto One Minus Div Nhds Within
lemma
proved
Curvature Roles
thesis/CESProofs/Applications/SettlementFeedback.lean
:459
Harmonic Mean Ge Half Min
lemma
proved
Curvature Roles
thesis/CESProofs/CurvatureRoles/Superadditivity.lean
:98
Concave On Nonneg Of Endpoints
lemma
proved
Curvature Roles
thesis/CESProofs/CurvatureRoles/Superadditivity.lean
:114
Rpow Concavity Deficit
lemma
proved
Curvature Roles
thesis/CESProofs/CurvatureRoles/Superadditivity.lean
:143
Bernoulli Rpow Ge Linear
lemma
proved
Curvature Roles
thesis/CESProofs/CurvatureRoles/Superadditivity.lean
:290
Gibbs Weight Has Deriv At
lemma
proved
Dynamics & Crises
thesis/CESProofs/Dynamics/GibbsMeasure.lean
:87
matTranspose_of_symmetric
lemma
proved
Dynamics & Crises
thesis/CESProofs/Dynamics/SymmetricAdjustment.lean
:64
isSymmetric_of_transpose_eq
lemma
proved
Dynamics & Crises
thesis/CESProofs/Dynamics/SymmetricAdjustment.lean
:69
matMul_transpose_general
lemma
proved
Dynamics & Crises
thesis/CESProofs/Dynamics/SymmetricAdjustment.lean
:75
matMul_assoc
lemma
proved
Dynamics & Crises
thesis/CESProofs/Dynamics/SymmetricAdjustment.lean
:81
matMul_transpose_of_symm
lemma
proved
Dynamics & Crises
thesis/CESProofs/Dynamics/SymmetricAdjustment.lean
:91
H J Sub One Pos
lemma
proved
Info Geometry
thesis/CESProofs/Foundations/CorrelationConvergence.lean
:78
Den Pos
lemma
proved
Info Geometry
thesis/CESProofs/Foundations/CorrelationConvergence.lean
:81
Has Deriv At Rpow
lemma
proved
Info Geometry
thesis/CESProofs/Foundations/CumulantTower.lean
:47
Has Deriv At Rpow Logpow
lemma
proved
Info Geometry
thesis/CESProofs/Foundations/CumulantTower.lean
:58
Multinomial QF
lemma
proved
Foundations
thesis/CESProofs/Foundations/GeneralHessian.lean
:96
Has Deriv At Rpow Exponent
lemma
proved
Info Geometry
thesis/CESProofs/Foundations/InformationGeometry.lean
:720
Has Deriv At Rpow Exponent Sq
lemma
proved
Info Geometry
thesis/CESProofs/Foundations/InformationGeometry.lean
:729
Quotient Rule Variance Eq
lemma
proved
Info Geometry
thesis/CESProofs/Foundations/InformationGeometry.lean
:777
Rpow Succ Pred
lemma
proved
Macroeconomics
thesis/CESProofs/Macro/DirectedTechnicalChange.lean
:129