Two-Level CES Curvature

def proved Dynamics & Crises

Documentation

Lean 4 Proof

def withinCurvature (w K : Fin N -> ℝ) : ℝ :=
  ∑ n, w n * K n

Dependency Graph

Used by

totalCurvature two_level_ces_curvature total_exceeds_within

Location

thesis/CESProofs/Dynamics/Closure.lean:58

Module Section

Results 80-85: Rho-Diversity Selection and Closure

In the same file

establishing rho_diversity_selection betweenCurvature totalCurvature two_level_ces_curvature between_curvature_pos total_exceeds_within industrial_policy_diversity closure_no_free_params closure_integrability closure_topological