Documentation

Lean 4 Proof

theorem factorShare_symmetric_uniform {J : ℕ} (hJ : 0 < J) {ρ : ℝ} {c : ℝ} (hc : 0 < c) :
    ∀ j : Fin J, factorShare J (fun _ => (1 : ℝ) / ↑J) ρ (symmetricPoint J c) j = 1 / ↑J := by
  intro j
  simp only [factorShare, symmetricPoint]
  have hJpos : (0 : ℝ) < ↑J := Nat.cast_pos.mpr hJ
  have hJne : (↑J : ℝ) ≠ 0 := ne_of_gt hJpos
  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:136

Module Section

Economics extensions for CES formalization:

In the same file