Documentation

Lean 4 Proof

theorem cross_level_amplification {N : ℕ} (k : Fin N → ℝ)
    (hk : ∀ n, 0 < k n)
    (hprod : 1 < ∏ n : Fin N, k n) :
    ∃ n, 1 < k n := by
  by_contra h
  push_neg at h
  have hle : ∏ n : Fin N, k n ≤ 1 := by
    calc ∏ n : Fin N, k n
        ≤ ∏ _n : Fin N, (1 : ℝ) := by
          exact Finset.prod_le_prod (fun n _ => le_of_lt (hk n)) (fun n _ => h n)
      _ = 1 := by simp
  linarith

Dependency Graph

Used by

Location

thesis/CESProofs/Hierarchy/Activation.lean:139

Module Section

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

In the same file