OAI/Computability/FourierTransform/FrameLifting.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PowerSaving.Binary.covered line 11

   Source documentation

   Portion of sigma occupied by the smaller network.

   def covered (e : ρ ↪ σ) := univ.map e
   …

2. theorem OAI.PowerSaving.Binary.cover_iff line 14
3. def OAI.PowerSaving.Binary.src line 16
4. theorem OAI.PowerSaving.Binary.src_spec line 20
5. theorem OAI.PowerSaving.Binary.src_self line 24
6. def OAI.PowerSaving.Binary.wide line 27
7. theorem OAI.PowerSaving.Binary.wide_both line 32
8. theorem OAI.PowerSaving.Binary.wide_in line 36
9. theorem OAI.PowerSaving.Binary.wide_out line 50
10. def OAI.PowerSaving.Binary.Move.over line 58
11. theorem OAI.PowerSaving.Binary.go_over line 63
12. theorem OAI.PowerSaving.Binary.go_out line 73
13. theorem OAI.PowerSaving.Binary.walk_over line 82
14. theorem OAI.PowerSaving.Binary.walk_out line 92
15. theorem OAI.PowerSaving.Binary.Path.lift line 102
16. theorem OAI.PowerSaving.Binary.Path.parallel line 146

    Source documentation

    Compose paths on disjoint sets of roles.

    theorem parallel (e : J → ρ ↪ σ)
        (dis : ∀ i j, i ≠ j → ∀ r ∈ covered (e i), r ∉ covered (e j))
        (A : σ → OBase α) {s t : σ → Finset α} {d : J → ℕ}
        {g : (σ→ℂ)→(σ→ℂ)} {h : J → (ρ→ℂ) → (ρ→ℂ)}
        (q : ∀ i, Path (A ∘ e i) (s ∘ e i) (t ∘ e i) (h i) (d i))
        (hin : ∀ i x, (g x) ∘ e i = h i (x ∘ e i))
        (hout : ∀ x r, (∀ i, r∉covered (e i)) → g x r=x r)
        (he : ∀ r, (∀ i, r∉covered (e i)) → s r=t r) :
        Path A s t g (∑ i, d i) := by
    …

    Mentions: OAI.PowerSaving.Binary.covered, OAI.PowerSaving.Binary.OBase, OAI.PowerSaving.Binary.Path