OAI/Computability/FourierCircuit/TensorTools.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ExactFourier.TensorTools.unit_reindex line 15
2. theorem OAI.ExactFourier.TensorTools.unit_tensor line 19
3. def OAI.ExactFourier.TensorTools.middleEquiv line 26
4. theorem OAI.ExactFourier.TensorTools.pad_middle line 32
5. theorem OAI.ExactFourier.TensorTools.pad_front line 42
6. theorem OAI.ExactFourier.TensorTools.join_mul line 52
7. theorem OAI.ExactFourier.TensorTools.price_join line 68
8. abbrev OAI.ExactFourier.CellJoin.join line 102
9. theorem OAI.ExactFourier.CellJoin.join_eq line 110
10. theorem OAI.ExactFourier.CellJoin.unit line 142
11. theorem OAI.ExactFourier.CellJoin.price line 148
12. def OAI.ExactFourier.Triangular.swapLast line 174
13. def OAI.ExactFourier.Triangular.liftEquiv line 180
14. def OAI.ExactFourier.Triangular.oldE line 183
15. theorem OAI.ExactFourier.Triangular.lift_identity line 186
16. theorem OAI.ExactFourier.Triangular.new_identity line 199
17. def OAI.ExactFourier.Triangular.nextE line 209
18. def OAI.ExactFourier.Triangular.mergeEquiv line 215
19. theorem OAI.ExactFourier.Triangular.merge_identity line 219
20. theorem OAI.ExactFourier.Triangular.next_price line 238
21. def OAI.ExactFourier.RowCompression.splitEquiv line 283

    Source documentation

    A chosen linear right inverse splits a surjection with its kernel.

    def splitEquiv (f : E →ₗ[K] F) (s : F →ₗ[K] E)
        (hs : f.comp s = LinearMap.id) : E ≃ₗ[K] F × LinearMap.ker f where
    …

22. theorem OAI.ExactFourier.RowCompression.splitEquiv_fst line 313
23. theorem OAI.ExactFourier.RowCompression.surjective_equiv line 318

    Source documentation

    Two surjections from the same finite-dimensional domain differ by an invertible change of domain. This is the block-copy coordinate change V.

    theorem surjective_equiv [FiniteDimensional K E] (f g : E →ₗ[K] F)
        (hf : Function.Surjective f) (hg : Function.Surjective g) :
        ∃ e : E ≃ₗ[K] E, ∀ x, f (e x) = g x := by
    …

24. theorem OAI.ExactFourier.RowCompression.range_equiv line 339

    Source documentation

    Equality of row spaces, not an assumption of full row rank, suffices.

    theorem range_equiv [FiniteDimensional K E] (f g : E →ₗ[K] F)
        (hfg : LinearMap.range f = LinearMap.range g) :
        ∃ e : E ≃ₗ[K] E, ∀ x, f (e x) = g x := by
    …

25. theorem OAI.ExactFourier.RowCompression.matrix_row_equiv line 358

    Source documentation

    The row-space equivalence as an actual invertible left multiplier.

    theorem matrix_row_equiv (R S : Matrix α β K)
        (hRS : Submodule.span K (Set.range R) = Submodule.span K (Set.range S)) :
        ∃ V : Matrix α α K, IsUnit V ∧ V * R = S := by
    …

26. theorem OAI.ExactFourier.RowCompression.sparse_row_compression line 383

    Source documentation

    Select a sparse spanning-family basis and perform the invertible compression on the whole row-block index. At most dim(β → K) rows remain.

    theorem sparse_row_compression {γ : Type*} [Fintype β] (R : Matrix α β K)
        (Q : γ → β → K)
        (hspan : Submodule.span K (Set.range R) = Submodule.span K (Set.range Q)) :
        ∃ V : Matrix α α K, IsUnit V ∧ ∃ I : Finset α,
          I.card ≤ Fintype.card β ∧
          (∀ i, i ∉ I → (V*R) i = 0) ∧
          (∀ i ∈ I, ∃ g, (V*R) i = Q g) := by
    …