OAI/Computability/FourierCircuit/SparseSpectral.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ExactFourier.SparseReflection.spectral_price line 12

   Source documentation

   Algebraic certificate for the real orthogonal reflection in the kernel, together with its uniform sparse price. Both annihilator equations are retained.

   theorem spectral_price (p : MatrixPrice) (A : Matrix α α ℝ) (hA : A.IsSymm)
       (d : α → ℂ) (L : List (PairTerm α))
       (hL : RealMatrix.complex A=Matrix.diagonal d+(L.map PairTerm.direction).sum) :
       ∃ R T : Matrix α α ℂ,R*R=1 ∧ R.IsSymm ∧
         RealMatrix.complex A*(1+R)=0 ∧ 1-R=RealMatrix.complex A*T ∧
         p.value R≤(3:ℝ)/2*L.length+2*Fintype.card α := by
   …

   Mentions: OAI.ExactFourier.MatrixPrice, OAI.ExactFourier.L, OAI.ExactFourier.SparseReflection.PairTerm, OAI.ExactFourier.RealMatrix.complex, OAI.ExactFourier.SparseReflection.PairTerm.direction

2. def OAI.ExactFourier.SparseReflection.pairs line 49
3. theorem OAI.ExactFourier.SparseReflection.mem_pairs line 51
4. def OAI.ExactFourier.SparseReflection.term line 53
5. def OAI.ExactFourier.SparseReflection.terms line 59
6. theorem OAI.ExactFourier.SparseReflection.terms_length line 62
7. theorem OAI.ExactFourier.SparseReflection.terms_sum line 64
8. theorem OAI.ExactFourier.SparseReflection.decomposition line 70
9. theorem OAI.ExactFourier.SparseReflection.twice_pairs_le line 89
10. theorem OAI.ExactFourier.SparseReflection.exists_reflection line 125

    Source documentation

    Uniform sparse reflection certificate, with supported unordered pairs counted exactly. The annihilator identities characterize the reflection when A is real symmetric.

    theorem exists_reflection (p : MatrixPrice) (A : Matrix α α ℂ) (hA : A.IsSymm)
        (hreal : ∀ i j,star (A i j)=A i j) :
        ∃ R T : Matrix α α ℂ,R*R=1 ∧ R.IsSymm ∧ A*(1+R)=0 ∧ 1-R=A*T ∧
          p.value R≤(3:ℝ)/2*(pairs A).card+2*Fintype.card α := by
    …

    Mentions: OAI.ExactFourier.MatrixPrice, OAI.ExactFourier.SparseReflection.pairs

11. theorem OAI.ExactFourier.SparseReflection.exists_reflection_nnz line 135
12. theorem OAI.ExactFourier.SymLap.relations line 155
13. theorem OAI.ExactFourier.SymLap.exists_tensor_reflection line 172
14. def OAI.ExactFourier.SignedBits.parity line 214
15. theorem OAI.ExactFourier.SignedBits.D_parity line 219
16. theorem OAI.ExactFourier.SignedBits.Gamma_parity line 233
17. def OAI.ExactFourier.SignedBits.paritySwitch line 245
18. theorem OAI.ExactFourier.SignedBits.paritySwitch_involutive line 249
19. def OAI.ExactFourier.SignedBits.parityEquiv line 252
20. theorem OAI.ExactFourier.SignedBits.parityEquiv_left line 255
21. theorem OAI.ExactFourier.SignedBits.parityEquiv_right line 259
22. def OAI.ExactFourier.GraphReflection.swap line 274
23. theorem OAI.ExactFourier.GraphReflection.swap_monomial line 276
24. theorem OAI.ExactFourier.GraphReflection.swap_square line 281
25. def OAI.ExactFourier.GraphReflection.hadamard line 283
26. theorem OAI.ExactFourier.GraphReflection.hadamard_square line 285
27. theorem OAI.ExactFourier.GraphReflection.hadamard_unit line 288
28. theorem OAI.ExactFourier.GraphReflection.hadamard_price line 294
29. def OAI.ExactFourier.GraphReflection.graph line 300
30. theorem OAI.ExactFourier.GraphReflection.graph_square line 302
31. theorem OAI.ExactFourier.GraphReflection.graph_price line 307
32. theorem OAI.ExactFourier.GraphReflection.gram_unit line 315
33. abbrev OAI.ExactFourier.SignedBits.Half line 330
34. def OAI.ExactFourier.SignedBits.tensorParityEquiv line 331
35. def OAI.ExactFourier.SignedBits.parityTensor line 335
36. theorem OAI.ExactFourier.SignedBits.parityTensor_square line 338
37. theorem OAI.ExactFourier.SignedBits.parityTensor_diag_left line 342
38. theorem OAI.ExactFourier.SignedBits.parityTensor_diag_right line 347
39. def OAI.ExactFourier.SignedBits.graphB line 352
40. theorem OAI.ExactFourier.SignedBits.graphB_unit line 354
41. theorem OAI.ExactFourier.SignedBits.parityTensor_graph line 362
42. theorem OAI.ExactFourier.SignedBits.graphB_real line 373