inv_phi_eq

formal source

  26noncomputable def paretoExponent : ℝ := 1 + phi⁻¹
  27
  28/-- 1/φ = φ - 1. -/
  29theorem inv_phi_eq : phi⁻¹ = phi - 1 := by
  30  have h := phi_sq_eq
  31  field_simp [phi_ne_zero]
  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