Documentation

Lean 4 Proof

theorem escort_uniform_at_symmetry {J : ℕ} (hJ : 0 < J)
    {c : ℝ} (hc : 0 < c) {ρ : ℝ} (_hρ : ρ ≠ 0) :
    ∀ _j : Fin J, c ^ ρ / (∑ _i : Fin J, c ^ ρ) = (1 : ℝ) / ↑J := by
  intro _
  have hcρ : 0 < c ^ ρ := Real.rpow_pos_of_pos hc ρ
  rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
  rw [div_eq_div_iff (ne_of_gt (mul_pos (Nat.cast_pos.mpr hJ) hcρ))
      (ne_of_gt (Nat.cast_pos.mpr hJ))]
  ring

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/Emergence.lean:403

Module Section

Emergence results from Paper 1, Sections 3-5:

In the same file