pith. machine review for the scientific record. sign in
theorem proved term proof

partition_function_positive

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  59theorem partition_function_positive (sys : DiscreteSystem) (T : ℝ) (hT : T > 0) :
  60    partitionFunction sys T hT > 0 := by

proof body

Term-mode proof.

  61  unfold partitionFunction
  62  have hne : Nonempty (Fin sys.numLevels) := ⟨⟨0, sys.nonempty⟩⟩
  63  apply Finset.sum_pos
  64  · intro i _
  65    apply mul_pos
  66    · -- degeneracy ≥ 1 > 0
  67      have h := sys.deg_pos i
  68      exact Nat.cast_pos.mpr (Nat.lt_of_lt_of_le Nat.zero_lt_one h)
  69    · exact exp_pos _
  70  · exact @Finset.univ_nonempty (Fin sys.numLevels) _ hne
  71
  72/-! ## Thermodynamic Quantities from Z -/
  73
  74/-- The Helmholtz free energy F = -k_B T ln Z. -/

depends on (17)

Lean names referenced from this declaration's body.