Documentation

Lean 4 Proof

theorem sensitivity_ratio_bottleneck {P k1 k2 : ℝ} (hP : 0 < P) (hk1 : 0 < k1) (_hk2 : 0 < k2)
    (h : k1 < k2) (n : ℕ) (hn : 0 < n) :
    P / (↑n * k2) < P / (↑n * k1) := by
  apply div_lt_div_of_pos_left hP
  · exact mul_pos (Nat.cast_pos.mpr hn) hk1
  · exact mul_lt_mul_of_pos_left h (Nat.cast_pos.mpr hn)

Dependency Graph

Location

thesis/CESProofs/Hierarchy/Activation.lean:172

Module Section

Theorems 5-6, Proposition 3: Next-Generation Matrix and Activation Threshold

In the same file