Sections / Section 3: Sextuple Role of Curvature K / dualExponent

Dual Exponent

defprovedFoundations

Documentation

Lean 4 Proof

def dualExponent (ρ : ℝ) : ℝ := ρ / (ρ - 1)

Dependency Graph

Used by

dualExponent_eq_conjExponent' shephards_lemma ces_demand_adding_up cesPriceIndex_def dualExponent_eq_sigma dualExponent_eq_conjExponent cesPriceIndex holder_conjugate_of_substitutes cesDemand_adding_up holder_ces_duality

Location

thesis/CESProofs/Foundations/FurtherProperties.lean:109

Module Section

Further properties of CES curvature (Paper 1, Section 9):

In the same file

cesThirdDerivValue ces_third_derivative_pos asymmetryRatio asymmetry_exceeds_one knockoutRetained knockout_partial_retained knockout_total_failure knockout_no_failure criticalFailures dualEigenvaluePerp curvature_conservation excessSavingCoeff substitution_savings