WeightedCycles.lean`

36 declarations, 0 contain sorry, 0 declared as axioms

def OAI.TorsionFreeZeroDivisors.WeightedCycles.weight line 12
Source documentation
Expanded length, attached to undirected edges.
```
def weight (w : Sym2 V → ℝ) (p : G.Walk u v) : ℝ := (p.edges.map w).sum
```
theorem OAI.TorsionFreeZeroDivisors.WeightedCycles.weight_nil line 14
theorem OAI.TorsionFreeZeroDivisors.WeightedCycles.weight_cons line 15
theorem OAI.TorsionFreeZeroDivisors.WeightedCycles.weight_append line 17
theorem OAI.TorsionFreeZeroDivisors.WeightedCycles.weight_reverse line 20
theorem OAI.TorsionFreeZeroDivisors.WeightedCycles.weight_nonneg line 23
theorem OAI.TorsionFreeZeroDivisors.WeightedCycles.weight_le_of_subwalk line 29
theorem OAI.TorsionFreeZeroDivisors.WeightedCycles.reduced_not_path_cycle line 38
Source documentation
A nonbacktracking walk with a repeated vertex contains a cycle of no greater weight. Zero weights are permitted.
```
theorem reduced_not_path_cycle (w : Sym2 V → ℝ) (hw : ∀ e, 0 ≤ w e)
    (r : G.Walk u v) (hrr : r.edges.IsChain (· ≠ ·)) (hn : ¬r.IsPath) :
    ∃ (a : V) (c : G.Walk a a), c.IsCycle ∧ weight w c ≤ weight w r := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.WeightedCycles.weight

theorem OAI.TorsionFreeZeroDivisors.WeightedCycles.reduced_isPath_of_weight_lt line 74

Source documentation

A nonbacktracking walk lighter than every cycle has no repeated vertex.

theorem reduced_isPath_of_weight_lt (w : Sym2 V → ℝ) (hw : ∀ e, 0 ≤ w e)
    (L : ℝ) (hG : ∀ a (c : G.Walk a a), c.IsCycle → L ≤ weight w c)
    (p : G.Walk u v) (hp : weight w p < L) (hred : p.edges.IsChain (· ≠ ·)) :
    p.IsPath := by
…

Mentions: OAI.TorsionFreeZeroDivisors.WeightedCycles.weight

theorem OAI.TorsionFreeZeroDivisors.WeightedCycles.distinct_reduced_cycle line 84
Source documentation
Two distinct immersed walks having the same endpoints contain a cycle whose expanded length is no greater than their combined expanded length.
```
theorem distinct_reduced_cycle (w : Sym2 V → ℝ) (hw : ∀ e, 0 ≤ w e)
    (p q : G.Walk u v) (hne : p ≠ q)
    (hp : p.edges.IsChain (· ≠ ·)) (hq : q.edges.IsChain (· ≠ ·)) :
    ∃ (a : V) (c : G.Walk a a), c.IsCycle ∧ weight w c ≤ weight w p + weight w q := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.WeightedCycles.weight
def OAI.TorsionFreeZeroDivisors.WeightedMoore.Chain line 105
Source documentation
A chain of k+1 directed edges, including chains of zero probability.
```
@[reducible] def Chain (D : Type*) : ℕ → Type _
  | 0 => D
  | k+1 => D × Chain D k
```
instance OAI.TorsionFreeZeroDivisors.WeightedMoore.(instance at line 109) line 109
def OAI.TorsionFreeZeroDivisors.WeightedMoore.head line 114
def OAI.TorsionFreeZeroDivisors.WeightedMoore.last line 118
def OAI.TorsionFreeZeroDivisors.WeightedMoore.cost line 122
def OAI.TorsionFreeZeroDivisors.WeightedMoore.mass line 126
structure OAI.TorsionFreeZeroDivisors.WeightedMoore.Transition line 133
Source documentation
A doubly stochastic transition rule, with no entry exceeding one half.
```
structure Transition : Prop where
…
```
theorem OAI.TorsionFreeZeroDivisors.WeightedMoore.mass_nonneg line 141
theorem OAI.TorsionFreeZeroDivisors.WeightedMoore.head_expectation line 148
Source documentation
Stationarity of uniform directed-edge measure, proved by finite summation.
```
theorem head_expectation (ht : Transition T) (k : ℕ) (f : D → ℝ) :
    ∑ p : Chain D k, mass T p * f (head p) = (∑ d, f d) / Fintype.card D := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.WeightedMoore.Transition, OAI.TorsionFreeZeroDivisors.WeightedMoore.Chain, OAI.TorsionFreeZeroDivisors.WeightedMoore.mass, OAI.TorsionFreeZeroDivisors.WeightedMoore.head
theorem OAI.TorsionFreeZeroDivisors.WeightedMoore.mass_sum line 172
theorem OAI.TorsionFreeZeroDivisors.WeightedMoore.cost_expectation line 176
theorem OAI.TorsionFreeZeroDivisors.WeightedMoore.mass_upper line 207

theorem OAI.TorsionFreeZeroDivisors.WeightedMoore.short_mass line 220

Source documentation

Finite Markov without probability-space infrastructure: at least half the mass has cost at most twice the expectation; zero-mass chains are irrelevant.

theorem short_mass {P : Type*} [Fintype P] (w c : P → ℝ)
    (hw : ∀ p, 0 ≤ w p) (hc : ∀ p, 0 ≤ c p)
    (hs : ∑ p, w p = 1) (B : ℝ) (hB : 0 < B)
    (hm : ∑ p, w p*c p ≤ B) :
    1/2 ≤ ∑ p ∈ Finset.univ.filter (fun p => c p ≤ 2*B ∧ 0 < w p), w p := by
…

theorem OAI.TorsionFreeZeroDivisors.WeightedMoore.cost_nonneg line 251
theorem OAI.TorsionFreeZeroDivisors.WeightedMoore.many_short_chains line 258
Source documentation
Entropy forces many short nonzero-probability nonbacktracking chains.
```
theorem many_short_chains [Nonempty D] (ht : Transition T) (k : ℕ)
    (len : D → ℝ) (hlen : ∀ d, 0 < len d) :
    ∃ S : Finset (Chain D k),
      (∀ p ∈ S, cost len p ≤ 2*(k+1:ℝ)*(∑ d, len d)/Fintype.card D ∧
        0 < mass T p) ∧
      (Fintype.card D : ℝ)*(2:ℝ)^k ≤ 2*S.card := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.WeightedMoore.Transition, OAI.TorsionFreeZeroDivisors.WeightedMoore.Chain, OAI.TorsionFreeZeroDivisors.WeightedMoore.cost, OAI.TorsionFreeZeroDivisors.WeightedMoore.mass
theorem OAI.TorsionFreeZeroDivisors.WeightedMoore.short_collision line 298
Source documentation
More short chains than ordered endpoint pairs forces a collision. This uses actual chains and their probabilities, not a hypothesis asserting path growth.
```
theorem short_collision [Nonempty D] (ht : Transition T) (k : ℕ)
    (len : D → ℝ) (hlen : ∀ d, 0 < len d)
    (hbig : 2*(Fintype.card D : ℝ) < (2:ℝ)^k) :
    ∃ p q : Chain D k, p ≠ q ∧ head p = head q ∧ last p = last q ∧
      0 < mass T p ∧ 0 < mass T q ∧
      cost len p + cost len q ≤ 4*(k+1:ℝ)*(∑ d, len d)/Fintype.card D := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.WeightedMoore.Transition, OAI.TorsionFreeZeroDivisors.WeightedMoore.Chain, OAI.TorsionFreeZeroDivisors.WeightedMoore.head, OAI.TorsionFreeZeroDivisors.WeightedMoore.last, OAI.TorsionFreeZeroDivisors.WeightedMoore.mass, OAI.TorsionFreeZeroDivisors.WeightedMoore.cost
theorem OAI.TorsionFreeZeroDivisors.WeightedMoore.logarithmic_short_collision line 324
Source documentation
An explicit logarithmic number of transitions suffices.
```
theorem logarithmic_short_collision [Nonempty D] (ht : Transition T)
    (len : D → ℝ) (hlen : ∀ d, 0 < len d) :
    let k := Nat.log 2 (Fintype.card D) + 2
…
```
Mentions: OAI.TorsionFreeZeroDivisors.WeightedMoore.Transition
def OAI.TorsionFreeZeroDivisors.WeightedMoore.PortWalk.out line 345
def OAI.TorsionFreeZeroDivisors.WeightedMoore.PortWalk.choices line 346
def OAI.TorsionFreeZeroDivisors.WeightedMoore.PortWalk.step line 348
def OAI.TorsionFreeZeroDivisors.WeightedMoore.PortWalk.transition line 350
theorem OAI.TorsionFreeZeroDivisors.WeightedMoore.PortWalk.succ_eq line 353
theorem OAI.TorsionFreeZeroDivisors.WeightedMoore.PortWalk.succ_card line 358
theorem OAI.TorsionFreeZeroDivisors.WeightedMoore.PortWalk.pred_eq line 365
theorem OAI.TorsionFreeZeroDivisors.WeightedMoore.PortWalk.pred_card line 381
theorem OAI.TorsionFreeZeroDivisors.WeightedMoore.PortWalk.transition_law line 389
Source documentation
The actual nonbacktracking chain on ports of a multigraph is stationary on uniformly chosen darts, including loops and parallel edges.
```
theorem transition_law (hdeg : ∀ d, 3 ≤ (out origin (origin d)).card) :
    Transition (transition origin rev) := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.WeightedMoore.PortWalk.out, OAI.TorsionFreeZeroDivisors.WeightedMoore.Transition, OAI.TorsionFreeZeroDivisors.WeightedMoore.PortWalk.transition