Documentation

Lean 4 Proof

theorem attractor_maximizes_renyi {J : ℕ} (hJ : 0 < J)
    {c : ℝ} (hc : 0 < c) {ρ : ℝ} (_hρ : ρ ≠ 0)
    {α : ℝ} (_hα₀ : 0 < α) (hα₁ : α ≠ 1) :
    let p : Fin J → ℝ := fun _ => c ^ ρ / (∑ _i : Fin J, c ^ ρ)
    (1 / (1 - α)) * Real.log (∑ j : Fin J, (p j) ^ α) = Real.log ↑J := by
  intro p
  have hJr : (0 : ℝ) < ↑J := Nat.cast_pos.mpr hJ
  have hJne : (↑J : ℝ) ≠ 0 := ne_of_gt hJr
  -- p j = 1/J for all j
  have hp_eq : ∀ j : Fin J, p j = 1 / ↑J :=
    escort_uniform_at_symmetry hJ hc _hρ
  -- Σ (1/J)^α = J · (1/J)^α
  have hsum_eq : ∑ j : Fin J, (p j) ^ α = ↑J * (1 / ↑J) ^ α := by
    simp_rw [hp_eq]
    rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
  rw [hsum_eq]
  -- J * (1/J)^α = J^{1-α}
  have halg : (↑J : ℝ) * (1 / ↑J : ℝ) ^ α = (↑J : ℝ) ^ (1 - α) := by
    conv_lhs => rw [show (↑J : ℝ) = (↑J : ℝ) ^ (1 : ℝ) from (rpow_one _).symm]
    rw [one_div, ← rpow_neg (le_of_lt hJr), ← rpow_mul (le_of_lt hJr),
        ← rpow_add hJr]
    congr 1; ring
  rw [halg, Real.log_rpow hJr]
  have h1a : (1 - α) ≠ 0 := sub_ne_zero.mpr (Ne.symm hα₁)
  field_simp

Dependency Graph

Location

thesis/CESProofs/Foundations/Emergence.lean:422

Module Section

Emergence results from Paper 1, Sections 3-5:

In the same file