OAI/Analysis/Unitarizability/SignMatrix.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Dixmier.SignMatrix.sum_on_embedding line 18
2. def OAI.Dixmier.SignMatrix.extend line 29
3. theorem OAI.Dixmier.SignMatrix.extend_apply line 32
4. theorem OAI.Dixmier.SignMatrix.extend_off line 36
5. theorem OAI.Dixmier.SignMatrix.sum_extend_sq line 39
6. def OAI.Dixmier.SignMatrix.vector line 43
7. theorem OAI.Dixmier.SignMatrix.vector_apply line 47
8. theorem OAI.Dixmier.SignMatrix.sign_sq line 50
9. theorem OAI.Dixmier.SignMatrix.vector_norm line 53
10. def OAI.Dixmier.SignMatrix.synthesis line 62
11. theorem OAI.Dixmier.SignMatrix.synthesis_apply line 66
12. def OAI.Dixmier.SignMatrix.testCoefficients line 70
13. theorem OAI.Dixmier.SignMatrix.testCoefficients_sq line 73
14. theorem OAI.Dixmier.SignMatrix.bilinear_test line 89
15. theorem OAI.Dixmier.SignMatrix.bilinear_tail line 107

    Source documentation

    The tail bound for each fixed pair of real unit test vectors and an injective coordinate selection, on the full sign-matrix sample space.

    theorem bilinear_tail [Nonempty K] (e : J ↪ I) (w : EuclideanSpace ℝ K) (z : EuclideanSpace ℝ J)
        (hw : ‖w‖ = 1) (hz : ‖z‖ = 1) :
        (((univ.filter fun σ : K × I → Bool => (5 : ℝ) < |inner ℝ (synthesis σ e z) w|).card : ℕ) : ℝ) /
          (2 : ℝ)^Fintype.card (K × I) ≤ 2 * Real.exp (-(Fintype.card K : ℝ)*25/2) := by
    …

    Mentions: OAI.Dixmier.SignMatrix.synthesis