Documentation

Lean 4 Proof

theorem qPartitionFun_pos_at_one (hJ : 0 < J) (T : ℝ) (_hT : 0 < T)
    (ε : Fin J → ℝ) :
    0 < qPartitionFun J 1 T ε := by
  simp only [qPartitionFun, qExp]
  apply Finset.sum_pos
  · intro j _
    simp only [↓reduceIte]
    exact exp_pos _
  · exact ⟨⟨0, hJ⟩, Finset.mem_univ _⟩

Dependency Graph

Location

thesis/CESProofs/Potential/Appendix.lean:79

Module Section

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

In the same file