Sections / Section 9: CES Potential and Information Friction / effectiveCurvatureKeff

Effective Curvature Keff

defprovedCES Potential

Documentation

Lean 4 Proof

def effectiveCurvatureKeff (J : ℕ) (ρ T Tstar : ℝ) : ℝ :=
  curvatureK J ρ * max 0 (1 - T / Tstar)

Dependency Graph

Used by

keff_below_critical landscape_structure keff_eq_K_times_reduced order_parameter_exponent_one liquidity_trap_escape sectorEffectiveCurvature keff_at_critical effectiveCurvatureKeff_nonneg institutions_dampen_spillover effectiveCurvatureKeff_pos bilateral_Keff_strict effectiveCurvatureKeff_above_critical currency_union_maximizes_Keff Keff_zero_at_critical recession_depth_proportional_to_K aggregation_rhoT multisector_stagflation effectiveMultiplier universality effectiveCurvatureKeff_zero_friction generalKeff_reduction_equal_weights recession_dual_degradation complementary_goods_higher_Keff effectiveCurvatureKeff_le_K landau_gives_keff bilateral_Keff_decreasing SextupleRoleStatement Keff_linear_near_critical keff_continuous hub_reform_benefits_all_spokes superadditivity_with_friction keff_slope_above institutional_amplification generalKeff_le_standardKeff highest_friction_pair_fails_first monetary_transmission_ordering policy_ineffective_above_critical policyResponse trade_collapse_at_critical bilateral_Keff_sq_decreasing efficiency_fragility_tradeoff keff_reduced_universal keff_slope_below

Location

thesis/CESProofs/Potential/Defs.lean:129

Module Section

Core definitions for the Lean formalization of Paper 2:

In the same file

qLog qExp qLog_one qExp_zero qLog_eq_of_ne qExp_eq_of_ne OnSimplex OnOpenSimplex tsallisEntropy tsallisEntropy_uniform cesPotential criticalFriction effectiveCurvatureKeff_zero_friction effectiveCurvatureKeff_above_critical effectiveCurvatureKeff_nonneg effectiveCurvatureKeff_le_K effectiveCurvatureKeff_pos uniform_onOpenSimplex OnOpenSimplex.toSimplex cesPotential_uniform_equal