Sections / alpha_self_dual_at_sigma_two

Alpha Self Dual At Sigma Two

theoremprovedFoundations

Documentation

Lean 4 Proof

theorem alpha_self_dual_at_sigma_two : alphaOfSigma 2 = 0 := by
  unfold alphaOfSigma; norm_num

Dependency Graph

Location

thesis/CESProofs/Foundations/TripleCorrespondence.lean:105

Module Section

### The Boltzmann-Escort Identification

In the same file

negEnergy boltzmann_eq_rpow boltzmann_eq_escort alphaOfSigma alpha_duality_involution alpha_at_cobb_douglas 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