Lean 4 Proof

theorem eigenvalue_T_Keff_pos {T : ℝ} {J : ℕ} {xbar K_eff : ℝ}
    (hT : 0 < T) (hJ : 2 ≤ J) (hx : 0 < xbar) (hK : 0 < K_eff) :
    0 < covEigenvaluePerp T J xbar K_eff := by
  simp only [covEigenvaluePerp]
  apply div_pos
  · have hJ' : (0 : ℝ) < ↑J := by exact_mod_cast (show (0 : ℕ) < J by omega)
    exact mul_pos (mul_pos hT hJ') (sq_pos_of_pos hx)
  · apply mul_pos hK
    have : (1 : ℝ) < ↑J := by exact_mod_cast (show 1 < J by omega)
    linarith

Dependency Graph

Location

thesis/CESProofs/Dynamics/ConservationLaws.lean:185

Module Section

Results 36-46: Conservation Laws and Symmetry Identities

In the same file