Documentation

Lean 4 Proof

theorem activation_two_level {k10 k21 : ℝ} (hk10 : 0 < k10) (hk21 : 0 < k21) :
    1 < Real.sqrt (k10 * k21) ↔ 1 < k10 * k21 := by
  constructor
  · intro h
    have hsq := sq_lt_sq' (by linarith : -Real.sqrt (k10 * k21) < 1) h
    rw [one_pow, sq_sqrt (mul_nonneg (le_of_lt hk10) (le_of_lt hk21))] at hsq
    exact hsq
  · intro h
    rw [show (1 : ℝ) = Real.sqrt 1 from (Real.sqrt_one).symm]
    exact Real.sqrt_lt_sqrt (by linarith) h

Dependency Graph

Location

thesis/CESProofs/Hierarchy/Activation.lean:42

Module Section

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

In the same file