theorem
proved
paretoExponent_eq_phi
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Economics.WealthDistributionFromSigma on GitHub at line 35.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
32 linarith
33
34/-- Pareto exponent = φ. -/
35theorem paretoExponent_eq_phi : paretoExponent = phi := by
36 unfold paretoExponent
37 rw [inv_phi_eq]
38 ring
39
40/-- Pareto exponent ∈ (1.61, 1.62). -/
41theorem paretoExponent_band :
42 (1.61 : ℝ) < paretoExponent ∧ paretoExponent < 1.62 := by
43 rw [paretoExponent_eq_phi]
44 exact ⟨phi_gt_onePointSixOne, phi_lt_onePointSixTwo⟩
45
46structure WealthDistributionCert where
47 exponent_eq_phi : paretoExponent = phi
48 exponent_band : (1.61 : ℝ) < paretoExponent ∧ paretoExponent < 1.62
49 inv_phi : phi⁻¹ = phi - 1
50
51noncomputable def wealthDistributionCert : WealthDistributionCert where
52 exponent_eq_phi := paretoExponent_eq_phi
53 exponent_band := paretoExponent_band
54 inv_phi := inv_phi_eq
55
56end IndisputableMonolith.Economics.WealthDistributionFromSigma