Documentation

Lean 4 Proof

theorem activation_threshold_iff_product {P_cycle : ℝ} (hP : 0 < P_cycle)
    {n : ℕ} (hn : 0 < n) :
    1 < P_cycle ^ ((1 : ℝ) / ↑n) ↔ 1 < P_cycle := by
  have hn_pos : (0 : ℝ) < ↑n := Nat.cast_pos.mpr hn
  rw [Real.one_lt_rpow_iff (le_of_lt hP)]
  constructor
  · intro h
    rcases h with ⟨h1, _⟩ | ⟨_, h2, h3⟩
    · exact h1
    · exfalso; linarith [div_pos one_pos hn_pos]
  · intro h
    left
    exact ⟨h, div_pos one_pos hn_pos⟩

Dependency Graph

Used by

Location

thesis/CESProofs/Hierarchy/Activation.lean:85

Module Section

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

In the same file