Sections / Section 11: Dynamics and Business Cycles / totalCurvature

Total Curvature

defprovedDynamics & Crises

Lean 4 Proof

def totalCurvature (w K : Fin N -> ℝ) (Ktilde VarRho : ℝ) : ℝ :=
  withinCurvature w K + betweenCurvature Ktilde VarRho

Dependency Graph

Used by

two_level_ces_curvature total_exceeds_within

Location

thesis/CESProofs/Dynamics/Closure.lean:64

Module Section

Results 80-85: Rho-Diversity Selection and Closure

In the same file

establishing rho_diversity_selection withinCurvature betweenCurvature two_level_ces_curvature between_curvature_pos total_exceeds_within industrial_policy_diversity closure_no_free_params closure_integrability closure_topological