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

Sensitivity Ratio

theoremprovedCES Potential

Documentation

Lean 4 Proof

theorem sensitivity_ratio {K : ℝ} (hK_pos : 0 < K) (hK_lt : K < 1) :
    K ^ 2 / K = K := by
  rw [sq, mul_div_cancel_of_imp]
  intro h; linarith

Dependency Graph

Location

thesis/CESProofs/Potential/EffectiveCurvature.lean:125

Module Section

Theorem 4 and Propositions 5-7, Corollary 1:

In the same file

effectiveCurvature_taylor superadditivity_with_friction correlation_robustness_degrades_faster crisis_sequence_ordering information_shadow degradation_monotone ces_prudence_with_friction adjustmentTimescale adjustmentTimescale_diverges adjustmentTimescale_monotone adjustmentTimescale_at_zero generalEffectiveCurvatureKeff generalCriticalFriction irsEffectiveCurvaturePerp irsCriticalFrictionPerp weightedKnockoutLoss expectedKnockoutLoss irsFirmProfit GeneralSubCritical ConcentratedRegime