Documentation

Lean 4 Proof

theorem crisis_sequence_ordering {x : ℝ} (hx_pos : 0 < x) (hx_lt : x < 1) :
    (1 - x) ^ 2 < (1 - x) := by
  have h1 : 0 < 1 - x := by linarith
  nlinarith [sq_nonneg x]

Dependency Graph

Used by

Location

thesis/CESProofs/Potential/EffectiveCurvature.lean:113

Module Section

Theorem 4 and Propositions 5-7, Corollary 1:

In the same file