Documentation

Lean 4 Proof

theorem diversity_can_activate {P_cycle : ℝ} (hP : 0 < P_cycle) :
    ∃ alpha : ℝ, 1 < alpha ∧ 1 < alpha * P_cycle := by
  refine ⟨max 2 (2 / P_cycle), ?_, ?_⟩
  · exact lt_of_lt_of_le one_lt_two (le_max_left 2 _)
  · by_cases h : P_cycle < 1
    · calc max 2 (2 / P_cycle) * P_cycle
          ≥ 2 / P_cycle * P_cycle := by
            exact mul_le_mul_of_nonneg_right (le_max_right _ _) (le_of_lt hP)
        _ = 2 := by field_simp
        _ > 1 := by norm_num
    · push_neg at h
      calc max 2 (2 / P_cycle) * P_cycle
          ≥ 2 * P_cycle := by
            exact mul_le_mul_of_nonneg_right (le_max_left _ _) (le_of_lt hP)
        _ ≥ 2 * 1 := by nlinarith
        _ > 1 := by norm_num

Dependency Graph

Location

thesis/CESProofs/Dynamics/HierarchicalJ.lean:61

Module Section

Paper 3c, Section 6: Hierarchical Implications

In the same file