Documentation

Lean 4 Proof

theorem cross_level_amplification_with_J {N : ℕ} (k : Fin N → ℝ)
    (hk : ∀ n, 0 < k n) (hprod : 1 < ∏ n : Fin N, k n) :
    ∃ n, 1 < k n :=
  cross_level_amplification k hk hprod

Dependency Graph

Location

thesis/CESProofs/Dynamics/HierarchicalJ.lean:146

Module Section

Paper 3c, Section 6: Hierarchical Implications

In the same file