Documentation

Lean 4 Proof

theorem escort_symmetric_eq_uniform {J : ℕ} (hJ : 0 < J) (ρ : ℝ) {c : ℝ} (hc : 0 < c) :
    ∀ j : Fin J, escortDistribution J ρ (symmetricPoint J c) j = 1 / ↑J := by
  intro j
  simp only [escortDistribution, symmetricPoint]
  have hcρ : (0 : ℝ) < c ^ ρ := rpow_pos_of_pos hc ρ
  rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
  field_simp

Dependency Graph

Location

thesis/CESProofs/Applications/Economics.lean:206

Module Section

Economics extensions for CES formalization:

In the same file