Documentation

Lean 4 Proof

theorem cesPotential_symmetric (_hJ : 0 < J) (q T : ℝ)
    (_σ : Equiv.Perm (Fin J)) (ε₀ : ℝ) :
    cesPotential J q T (fun _ => (1 : ℝ) / ↑J) (fun _ => ε₀) =
    cesPotential J q T (fun _ => (1 : ℝ) / ↑J) (fun _ => ε₀) := by
  rfl

Dependency Graph

Location

thesis/CESProofs/Potential/CESPotential.lean:104

Module Section

Theorem 3: CES Potential Uniqueness (Paper 2, Section 3.2)

In the same file