Documentation

Lean 4 Proof

theorem qPartitionFun_equal_payoffs (q T ε₀ : ℝ) :
    qPartitionFun J q T (fun _ => ε₀) = ↑(Fintype.card (Fin J)) * qExp q (ε₀ / T) := by
  simp [qPartitionFun, Finset.sum_const, nsmul_eq_mul]

Dependency Graph

Location

thesis/CESProofs/Potential/Appendix.lean:90

Module Section

Appendix Lemmas 1-3 (Paper 2, Appendix A)

In the same file