Documentation

Lean 4 Proof

theorem stability_mode_contraction {k : ℕ} (hk : 2 ≤ k) {m₁ m₂ : ℕ}
    (hm₁ : 3 ≤ m₁) (hm₂ : m₁ ≤ m₂) :
    modeRate k m₂ ≤ modeRate k m₁ := by
  rcases eq_or_lt_of_le hm₂ with rfl | hlt
  · exact le_refl _
  · simp only [modeRate, if_neg (show ¬(m₁ ≤ 2) by omega),
               if_neg (show ¬(m₂ ≤ 2) by omega)]
    apply Real.rpow_le_rpow_of_exponent_le
    · exact_mod_cast (show 1 ≤ k by omega)
    · apply div_le_div_of_nonneg_right _ (by positivity : (0:ℝ) ≤ 2)
      simp only [neg_le_neg_iff]
      exact_mod_cast (show m₁ - 2 ≤ m₂ - 2 by omega)

Dependency Graph

Location

thesis/CESProofs/Foundations/Emergence.lean:206

Module Section

Emergence results from Paper 1, Sections 3-5:

In the same file