Curvature K

def proved Foundationskey theorem

Documentation

Lean 4 Proof

def curvatureK (J : ℕ) (ρ : ℝ) : ℝ := (1 - ρ) * (↑J - 1) / ↑J

Dependency Graph

Used by

sectionalCurvature_from_K keff_below_critical landscape_structure premium_factor_eq_K_scaled relative_has_positive_K_sensitivity cesMultiplier strategic_bound keff_eq_K_times_reduced order_parameter_exponent_one curvatureK_increment curvature_alt_form dual_curvature_principle quadratic_channel_zero_at_linear regime_trichotomy eos_curvature_determines_step equal_weight_entry_improves_K indicator_classification_foundations currency_union_maximizes_Keff curvatureK_eq_zero_of_rho_one levelStandardCurvature curvatureK_eq_sigma fifth_role_of_K recession_depth_proportional_to_K aggregation_rhoT curvatureK_from_hessLogF diversity_encoding criticalFriction curvatureK_real_eq_nat slope_jump_pos more_sectors_more_information curvatureK_eq_via_sigma universality information_shadow K_deficit_from_concentration effectiveCurvatureKeff_zero_friction complementary_sectors_highest_return williamson_special_case hessianQF_eq_negK_norm estimation_precision_bridge equal_weight_entry_maximizes_K curvatureKReal_eq_nat effectiveCurvatureKeff_le_K curvatureK_abs_substitute curvatureK_eq_curvatureKH landau_gives_keff effectiveCurvatureKeff rho_ordering_criticalFriction asymmetryRatio trivial_fixed_point_at_rho_one SextupleRoleStatement sectorCurvature Keff_linear_near_critical phillips_flattening effectiveCurvature_le_K cesThirdDerivValue superadditivity_with_friction curvatureK_pos detection_achievable curvatureK_mul_sigma K_increases_with_complementarity aggregate_has_zero_K_sensitivity powerMean_mono_curvature equal_weights_maximize_K curvatureK_eq_bridge_times_fisher effectiveCurvature_at_symmetry manipulation_magnitude curvatureK_sign_classification excessSavingCoeff curvatureK_neg_substitute relaxation_rate_vanishes_at_Tstar curvatureK_two_factor_pos complementarity_alignment no_tradeoff_welfare_interpretation curvatureK_two_factor monetary_transmission_ordering nontrivial_fixed_point_iff cesCriticalStep_via_curvatureK complementary_goods_more_fragile eigenvaluePerp_sq_proportional_to_K_sq curvatureK_decreasing_in_rho K_reduction_equal_weights detectionThresholdLHS slope_jump_magnitude curvature_is_aversion_times_diversity equalWeights_maximize_K substitution_savings quadratic_channel_present deviationGain_eq_K keff_reduced_universal keff_slope_below

Location

thesis/CESProofs/Foundations/Defs.lean:66

Module Section

Core definitions for the Lean formalization of Paper 1: