Sections / alpha_at_cobb_douglas

Alpha At Cobb Douglas

theoremprovedFoundations

Documentation

Lean 4 Proof

theorem alpha_at_cobb_douglas : alphaOfSigma 1 = -1 := by
  unfold alphaOfSigma; norm_num

Dependency Graph

Location

thesis/CESProofs/Foundations/TripleCorrespondence.lean:112

Module Section

### The Boltzmann-Escort Identification

In the same file

negEnergy boltzmann_eq_rpow boltzmann_eq_escort alphaOfSigma alpha_duality_involution alpha_self_dual_at_sigma_two shannonEntropy escortEntropy efficiencyTerm specificHeat logZ_eq_rho_eff_plus_entropy free_energy_decomposition specific_heat_zero_at_symmetry alphaDivergence pareto_set_eflat projection_equilibrium pythagorean_welfare fisherCESMetricDiag mechanism_efficiency_bound complementarity_sharpens_prices