OAI/Combinatorics/Sensitivity/HammingBase.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Paper320.hammingDist_flip_self line 14
2. theorem OAI.Paper320.hammingDist_le_flip_add_one line 25
3. theorem OAI.Paper320.hammingDist_flip_le_add_one line 31
4. theorem OAI.Paper320.hammingDist_flip_eq_add_one line 37
5. def OAI.Paper320.ballPredicate line 51

   Source documentation

   The union of equal-radius Hamming balls.

   def ballPredicate [Fintype C] (centers : C → I → Bool) (R : ℕ)
       (x : I → Bool) : Bool :=
   …

6. theorem OAI.Paper320.ballPredicate_eq_true line 55
7. theorem OAI.Paper320.ballPredicate_nested line 60
8. theorem OAI.Paper320.ballPredicate_zero_flip line 66
9. theorem OAI.Paper320.near_center_unique line 81
10. theorem OAI.Paper320.ballPredicate_sensitivityAt_zero_le line 91
11. theorem OAI.Paper320.ballPredicate_no_joint_zero line 115
12. theorem OAI.Paper320.ballPredicate_no_joint_one line 124
13. def OAI.Paper320.nearestDistance line 134

    Source documentation

    Minimum distance to the finite nonempty family of centers.

    def nearestDistance [Fintype C] [Nonempty C] (centers : C → I → Bool)
        (x : I → Bool) : ℕ :=
    …

14. theorem OAI.Paper320.ballPredicate_eq_nearestDistance line 138
15. theorem OAI.Paper320.nearestDistance_le_flip_add_one line 143