OAI/Probability/CriticalZ3/Matching.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.GreedyPacking.exists_packing line 18

   Source documentation

   Greedily deleting at most M conflicts loses at most M elements per choice.

   theorem exists_packing (t : Finset α) (R : α → α → Prop)
       (hrefl : ∀ a ∈ t, R a a) (hsym : ∀ a ∈ t, ∀ b ∈ t, R a b → R b a)
       (M : ℕ) (hM : ∀ a ∈ t, (t.filter (R a)).card ≤ M) :
       ∃ s : Finset α, s ⊆ t ∧ (s : Set α).Pairwise (fun a b => ¬R a b) ∧ t.card ≤ M*s.card := by
   …

2. theorem OAI.GreedyPacking.exists_packing_card line 52

   Source documentation

   The prescribed K choices exist once there are K M candidates.

   theorem exists_packing_card (t : Finset α) (R : α → α → Prop)
       (hrefl : ∀ a ∈ t, R a a) (hsym : ∀ a ∈ t, ∀ b ∈ t, R a b → R b a)
       (M K : ℕ) (hM0 : 0 < M) (hM : ∀ a ∈ t, (t.filter (R a)).card ≤ M)
       (ht : K*M ≤ t.card) :
       ∃ s : Finset α, s ⊆ t ∧ s.card = K ∧ (s : Set α).Pairwise (fun a b => ¬R a b) := by
   …

3. def OAI.FiniteMatching.incident line 68
4. def OAI.FiniteMatching.conflict line 71
5. theorem OAI.FiniteMatching.conflict_refl line 75
6. theorem OAI.FiniteMatching.conflict_symm line 78
7. theorem OAI.FiniteMatching.conflict_card line 82
8. theorem OAI.FiniteMatching.exists_matching line 98
9. theorem OAI.FiniteMatching.endpoint_injective line 108
10. def OAI.PlanarBoundary.primalInside line 127
11. def OAI.PlanarBoundary.primalOutside line 128
12. theorem OAI.PlanarBoundary.boundary_degree line 131

    Source documentation

    Boundary edges incident to a fixed primal vertex have at most four possibilities.

    theorem boundary_degree (X : Finset Point) (v : Point) :
        Fintype.card {e : Boundary X // primalInside e = v ∨ primalOutside e = v} ≤ 4 := by
    …

    Mentions: OAI.PlanarBoundary.Point, OAI.PlanarBoundary.Boundary, OAI.PlanarBoundary.primalInside, OAI.PlanarBoundary.primalOutside

13. def OAI.PlanarBoundary.Valid line 156
14. def OAI.PlanarBoundary.inner line 160
15. def OAI.PlanarBoundary.outer line 161
16. theorem OAI.PlanarBoundary.code_degree line 164
17. theorem OAI.PlanarBoundary.exists_code_matching line 184