OAI/Combinatorics/SharpThreshold/SupportIncidence.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem313.support_vertices_image line 12
2. lemma OAI.Problem313.support_degree_image line 17
3. lemma OAI.Problem313.graph_support_vertices_card_le line 25
4. lemma OAI.Problem313.exists_graph_support_degree_sq_le line 36
5. lemma OAI.Problem313.exists_graph_support_degree_le line 54

   Source documentation

   The graph support vertex needed in block-capture, already in the real cutoff form.

   lemma exists_graph_support_degree_le {n : ℕ} (S : Finset (GraphEdge n))
       (hne : S.Nonempty) {k : ℝ} (hk : 0 ≤ k)
       (hcard : (S.card : ℝ) ≤ k ^ 2 / 2) :
       ∃ u ∈ S.biUnion Subtype.val,
         1 ≤ (S.filter (fun e => u ∈ e.val)).card ∧
         ((S.filter (fun e => u ∈ e.val)).card : ℝ) ≤ k := by
   …

   Mentions: OAI.Problem313.GraphEdge

6. lemma OAI.Problem313.graph_support_vertices_card_le_cutoff line 66