Documentation

Lean 4 Proof

theorem perron_frobenius_monotone {N : ℕ} (hN : 0 < N)
    (k₁ k₂ : Fin N → ℝ) (hk₁ : ∀ n, 0 < k₁ n)
    (h_le : ∀ n, k₁ n ≤ k₂ n) (h_strict : ∃ n, k₁ n < k₂ n) :
    (∏ n : Fin N, k₁ n) ^ ((1 : ℝ) / ↑N) <
    (∏ n : Fin N, k₂ n) ^ ((1 : ℝ) / ↑N) := by
  have hprod_lt : ∏ n : Fin N, k₁ n < ∏ n : Fin N, k₂ n := by
    apply Finset.prod_lt_prod (fun n _ => hk₁ n) (fun n _ => h_le n)
    obtain ⟨m, hm⟩ := h_strict
    exact ⟨m, Finset.mem_univ m, hm⟩
  have hprod_nonneg : (0 : ℝ) ≤ ∏ n : Fin N, k₁ n :=
    le_of_lt (Finset.prod_pos fun n _ => hk₁ n)
  have hexp_pos : (0 : ℝ) < 1 / ↑N := div_pos one_pos (Nat.cast_pos.mpr hN)
  exact Real.rpow_lt_rpow hprod_nonneg hprod_lt hexp_pos

Dependency Graph

Location

thesis/CESProofs/Hierarchy/EndogenousCrossing.lean:136

Module Section

Proposition: Endogenous Crossing

In the same file