OAI/Combinatorics/GotsmanLinial/Statement.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LeanBlast.GotsmanLinial.flip_apply_same line 9
2. theorem OAI.LeanBlast.GotsmanLinial.flip_apply_ne line 13
3. theorem OAI.LeanBlast.GotsmanLinial.flip_flip line 17
4. theorem OAI.LeanBlast.GotsmanLinial.flip_ne_self line 25
5. theorem OAI.LeanBlast.GotsmanLinial.flip_injective_direction line 30
6. theorem OAI.LeanBlast.GotsmanLinial.flip_involutive line 37
7. theorem OAI.LeanBlast.GotsmanLinial.flip_bijective line 40
8. theorem OAI.LeanBlast.GotsmanLinial.cubeCoord_flip_same line 43
9. theorem OAI.LeanBlast.GotsmanLinial.cubeCoord_flip_ne line 47
10. theorem OAI.LeanBlast.GotsmanLinial.cubeCoord_cases line 51
11. theorem OAI.LeanBlast.GotsmanLinial.cubeCoord_sq line 55
12. theorem OAI.LeanBlast.GotsmanLinial.thresholdSign_zero line 59
13. theorem OAI.LeanBlast.GotsmanLinial.thresholdSign_eq_one_iff line 62
14. theorem OAI.LeanBlast.GotsmanLinial.thresholdSign_eq_neg_one_iff line 67
15. theorem OAI.LeanBlast.GotsmanLinial.thresholdSign_cases line 72
16. theorem OAI.LeanBlast.GotsmanLinial.thresholdSign_sq line 76
17. theorem OAI.LeanBlast.GotsmanLinial.card_cube line 79
18. def OAI.LeanBlast.GotsmanLinial.cubeEquivSignVectors line 83

    Source documentation

    The Boolean encoding represents every sign vector exactly once.

    noncomputable def cubeEquivSignVectors (n : ℕ) :
        Cube n ≃ {x : Fin n → ℝ // ∀ i, x i = 1 ∨ x i = -1} := by
    …

    Mentions: OAI.LeanBlast.GotsmanLinial.Cube

19. theorem OAI.LeanBlast.GotsmanLinial.averageSensitivity_eq_count line 100
20. theorem OAI.LeanBlast.GotsmanLinial.averageSensitivity_eq_uniform line 104