Documentation

Lean 4 Proof

theorem ces_log_supermodular (J : ℕ) {ρ : ℝ} (hρ : ρ < 1)
    {c : ℝ} (hc : 0 < c) (hJ : 0 < J)
    {i j : Fin J} (hij : i ≠ j) :
    0 < cesHessianEntry J ρ c i j := by
  simp only [cesHessianEntry, hij, ite_false, sub_zero, mul_one]
  apply div_pos
  · linarith
  · apply mul_pos
    · positivity
    · exact hc

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/Strategic.lean:34

Module Section

Strategic independence of CES (Paper 1, Sections 7-8):

In the same file