OAI/Analysis/Matrix/BlockCycles.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CoordinateSweeps.BlockCycles.tupleSplit line 24
2. lemma OAI.CoordinateSweeps.BlockCycles.sum_tuple_split line 31
3. def OAI.CoordinateSweeps.BlockCycles.walk line 36
4. lemma OAI.CoordinateSweeps.BlockCycles.walk_succ line 40
5. lemma OAI.CoordinateSweeps.BlockCycles.snoc_cons line 46
6. lemma OAI.CoordinateSweeps.BlockCycles.product_entry line 59

   Source comment

   Complete matrix product expansion by paths, with the endpoint checked rather than divided out. Valid for any noncommutative semiring of blocks.

   lemma product_entry {n : ℕ} (A : Fin n → Matrix Ω Ω R) (i j : Ω) :
       ((List.ofFn A).prod) i j=
         ∑ x : Fin n → Ω, if (Fin.snoc (α := fun _ => Ω) x j) 0=i then walk A (Fin.snoc (α := fun _ => Ω) x j) else 0 := by
   …

   Mentions: OAI.CoordinateSweeps.BlockCycles.walk

7. lemma OAI.CoordinateSweeps.BlockCycles.snoc_cycle line 89
8. theorem OAI.CoordinateSweeps.BlockCycles.trace_product line 102

   Source comment

   Exact cyclic trace expansion, also when entries themselves are matrices.

   theorem trace_product {n : ℕ} (A : Fin (n+1) → Matrix Ω Ω R) :
       Matrix.trace ((List.ofFn A).prod)=
         ∑ x : Fin (n+1) → Ω, (List.ofFn (fun i => A i (x i) (x (i+1)))).prod := by
   …

9. def OAI.CoordinateSweeps.BlockCycles.block line 126
10. def OAI.CoordinateSweeps.BlockCycles.blocks line 130

    Source comment

    Literal placement blocks, with no normalized trace convention.

    def blocks : Matrix (Ω × n) (Ω × n) R →+* Matrix Ω Ω (Matrix n n R) where
    …

11. lemma OAI.CoordinateSweeps.BlockCycles.blocks_apply line 147
12. lemma OAI.CoordinateSweeps.BlockCycles.trace_blocks line 150
13. theorem OAI.CoordinateSweeps.BlockCycles.trace_block_product line 156

    Source comment

    Exact placement-cycle expansion of a product of operators on placement fibers.

    theorem trace_block_product {m : ℕ} [NeZero m] (hm : 0 < m)
        (A : Fin m → Matrix (Ω × n) (Ω × n) R) :
        Matrix.trace (List.ofFn A).prod=
          ∑ x : Fin m → Ω, Matrix.trace (List.ofFn (fun i => blocks (A i) (x i) (x (i+1)))).prod := by
    …

    Mentions: OAI.CoordinateSweeps.BlockCycles.blocks

14. theorem OAI.CoordinateSweeps.BlockCycles.trace_block_holder line 175

    Source comment

    Trace Holder applied separately on every literal placement cycle.

    theorem trace_block_holder {m : ℕ} [NeZero m] (hm : 0 < m)
        (A : Fin m → Matrix (Ω × n) (Ω × n) ℂ) :
        ‖Matrix.trace (List.ofFn A).prod‖ ≤
          ∑ x : Fin m → Ω, ∏ i, schatten m (blocks (A i) (x i) (x (i+1))) := by
    …

    Mentions: OAI.CoordinateSweeps.BlockCycles.blocks

15. def OAI.CoordinateSweeps.BlockCycles.evenWord line 183

    Source comment

    The exact alternating word for the unnormalized even moment.

    def evenWord (q : ℕ) (A : Matrix (Ω × n) (Ω × n) ℂ) : List (Matrix (Ω × n) (Ω × n) ℂ) :=
    …

16. lemma OAI.CoordinateSweeps.BlockCycles.evenWord_length line 187
17. lemma OAI.CoordinateSweeps.BlockCycles.evenWord_prod line 192
18. lemma OAI.CoordinateSweeps.BlockCycles.evenWord_mem line 201
19. theorem OAI.CoordinateSweeps.BlockCycles.even_moment_blocks line 209

    Source comment

    Literal cyclic index expansion of the induced even moment, before probabilities and augmented path potentials are substituted.

    theorem even_moment_blocks (q : ℕ) (hq : 0 < q) (A : Matrix (Ω × n) (Ω × n) ℂ) :
        let L := evenWord q A
    …

    Mentions: OAI.CoordinateSweeps.BlockCycles.evenWord

20. def OAI.CoordinateSweeps.BlockCycles.edgeWeight line 238
21. def OAI.CoordinateSweeps.BlockCycles.edgeFiber line 241
22. lemma OAI.CoordinateSweeps.BlockCycles.block_adjoint line 246
23. lemma OAI.CoordinateSweeps.BlockCycles.edge_block line 250
24. lemma OAI.CoordinateSweeps.BlockCycles.edgeWeight_nonneg line 265
25. theorem OAI.CoordinateSweeps.BlockCycles.even_cycle_bound line 272

    Source comment

    Each placement cycle carries exactly the transition probabilities of its forward or adjoint edges and the unnormalized conditional fiber moments.

    theorem even_cycle_bound (q : ℕ) (hq : 0 < q) (A : Matrix (Ω × n) (Ω × n) ℂ)
        (p : Ω → Ω → ℝ) (hp : ∀ y x, 0 ≤ p y x) (K : Ω → Ω → Matrix n n ℂ)
        (hA : ∀ y x, blocks A y x=(p y x : ℂ) • K y x) :
        let L := evenWord q A
    …

    Mentions: OAI.CoordinateSweeps.BlockCycles.blocks, OAI.CoordinateSweeps.BlockCycles.evenWord