OAI/Probability/CriticalZ3/FiniteTrails.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteTrails.successor line 17
2. theorem OAI.FiniteTrails.successor_tail line 24
3. theorem OAI.FiniteTrails.exists_cycle_nonzero line 30

   Source documentation

   Some cycle class has nonzero weight whenever the total weight does.

   theorem exists_cycle_nonzero (σ : Equiv.Perm D) (w : D → ℤ)
       (hw : ∑ d, w d ≠ 0) :
       ∃ d, (∑ e : D, if σ.SameCycle d e then w e else 0) ≠ 0 := by
   …

4. theorem OAI.FiniteTrails.period_pos line 56
5. def OAI.FiniteTrails.cycleEquiv line 59
6. def OAI.FiniteTrails.next line 78
7. theorem OAI.FiniteTrails.exists_closed_trail line 82

   Source documentation

   A closed trail has distinct edges and retains the nonzero marked crossing sum.

   theorem exists_closed_trail (tail head : D → V)
       (hbal : ∀ v, Fintype.card {d // head d = v} = Fintype.card {d // tail d = v})
       (w : D → ℤ) (hw : ∑ d, w d ≠ 0) :
       ∃ n : ℕ, ∃ hn : 0 < n, ∃ e : Fin n → D, Function.Injective e ∧
         (∀ i : Fin n, tail (e (next hn i)) = head (e i)) ∧ (∑ i, w (e i)) ≠ 0 := by
   …

   Mentions: OAI.FiniteTrails.next