OAI/Probability/GammaPassage/OrientedSelection.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarFPP.orientedSelectionBox line 13
2. theorem OAI.PlanarFPP.orientedSelectionBox_card line 16
3. theorem OAI.PlanarFPP.separated_selection line 23

   Source documentation

   Greedy selection in a finite symmetric neighborhood system.

   Also declared: OAI/Probability/FirstPassage/SeparatedSelection.lean:8 (same declaration text).

   theorem separated_selection {α : Type*} (R : α → α → Prop) [DecidableRel R]
       (hrefl : ∀ a, R a a) (hsymm : ∀ a b, R a b → R b a)
       (S : Finset α) (d : ℕ)
       (hdegree : ∀ a ∈ S, (S.filter (R a)).card ≤ d) :
       ∃ T : Finset α, T ⊆ S ∧
         Set.Pairwise (↑T : Set α) (fun a b => ¬R a b) ∧ S.card ≤ d*T.card := by
   …

4. def OAI.PlanarFPP.latticeNear line 66

   Also declared: OAI/Probability/FirstPassage/SeparatedSelection.lean:51 (same declaration text).

5. instance OAI.PlanarFPP.(instance at line 69) line 69
6. theorem OAI.PlanarFPP.latticeNear_refl line 72

   Also declared: OAI/Probability/FirstPassage/SeparatedSelection.lean:57 (same declaration text).

7. theorem OAI.PlanarFPP.latticeNear_symm line 75

   Also declared: OAI/Probability/FirstPassage/SeparatedSelection.lean:60 (same declaration text).

8. theorem OAI.PlanarFPP.near_filter_card_le line 80

   Distinct definitions of this name: OAI/Probability/FirstPassage/SeparatedSelection.lean:65 (same statement text; different proof or body). Qualify references as OAI.PlanarFPP.near_filter_card_le@path.

9. theorem OAI.PlanarFPP.lattice_separated_selection line 94

   Source documentation

   From N sites, retain a pairwise k-separated subfamily of size at least N/(2k+1)^2, expressed without integer division or rounding loss.

   Also declared: OAI/Probability/FirstPassage/SeparatedSelection.lean:77 (same declaration text).

   theorem lattice_separated_selection (S : Finset Vertex) (k : ℕ) :
       ∃ T : Finset Vertex, T ⊆ S ∧
         Set.Pairwise (↑T : Set Vertex) (fun p q => ¬latticeNear k p q) ∧
         S.card ≤ (2*k+1)^2*T.card := by
   …

   Mentions: OAI.PlanarFPP.Vertex, OAI.PlanarFPP.latticeNear