Documentation

Lean 4 Proof

theorem J_scaling_raises_cycle_product {N : ℕ} (hN : 0 < N)
    {alpha : ℝ} (halpha : 1 < alpha)
    {k : Fin N → ℝ} (hk : ∀ n, 0 < k n) :
    ∏ n : Fin N, k n < ∏ n : Fin N, alpha * k n := by
  rw [cycle_product_scales_with_J]
  have hprod : 0 < ∏ n : Fin N, k n := Finset.prod_pos fun n _ => hk n
  have haN : 1 < alpha ^ N := one_lt_pow₀ halpha (by omega : N ≠ 0)
  nlinarith

Dependency Graph

Location

thesis/CESProofs/Dynamics/HierarchicalJ.lean:49

Module Section

Paper 3c, Section 6: Hierarchical Implications

In the same file