BlockIncidence.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem313.block_filter_eq_vertex_filter line 11

Source documentation

If a block meets the vertex support in one vertex, precisely that vertex's incident support edges survive restriction to the block.

theorem block_filter_eq_vertex_filter {n : ℕ}
    (S : Finset (GraphEdge n)) (B : Finset (Fin n)) (u : Fin n)
    (h : B ∩ S.biUnion (fun e => e.val) = {u}) :
    S.filter (fun e => (e.val ∩ B).Nonempty) =
      S.filter (fun e => u ∈ e.val) := by
…

Mentions: OAI.Problem313.GraphEdge

theorem OAI.Problem313.block_filter_card_eq_vertex_degree line 34

Source documentation

Cardinal version of deterministic capture by a singleton vertex intersection.

theorem block_filter_card_eq_vertex_degree {n : ℕ}
    (S : Finset (GraphEdge n)) (B : Finset (Fin n)) (u : Fin n)
    (h : B ∩ S.biUnion (fun e => e.val) = {u}) :
    (S.filter (fun e => (e.val ∩ B).Nonempty)).card =
      (S.filter (fun e => u ∈ e.val)).card := by
…

Mentions: OAI.Problem313.GraphEdge

theorem OAI.Problem313.block_captures_of_singleton_inter line 43

Source documentation

The singleton-intersection event detects every support with a vertex of degree between one and the requested cutoff.

theorem block_captures_of_singleton_inter {n : ℕ}
    (S : Finset (GraphEdge n)) (B : Finset (Fin n)) (u : Fin n) (k : ℝ)
    (h : B ∩ S.biUnion (fun e => e.val) = {u})
    (hpos : 1 ≤ (S.filter (fun e => u ∈ e.val)).card)
    (hdeg : ((S.filter (fun e => u ∈ e.val)).card : ℝ) ≤ k) :
    1 ≤ (S.filter (fun e => (e.val ∩ B).Nonempty)).card ∧
      ((S.filter (fun e => (e.val ∩ B).Nonempty)).card : ℝ) ≤ k := by
…

Mentions: OAI.Problem313.GraphEdge

theorem OAI.Problem313.block_not_disjoint_filter_eq_vertex_filter line 54

Source documentation

The same capture identity with the disjointness predicate used for free edges.

theorem block_not_disjoint_filter_eq_vertex_filter {n : ℕ}
    (S : Finset (GraphEdge n)) (B : Finset (Fin n)) (u : Fin n)
    (h : B ∩ S.biUnion (fun e => e.val) = {u}) :
    S.filter (fun e => ¬Disjoint e.val B) =
      S.filter (fun e => u ∈ e.val) := by
…

Mentions: OAI.Problem313.GraphEdge

theorem OAI.Problem313.block_inter_free_edges_eq_vertex_filter line 64

Source documentation

The free-edge intersection formulation of deterministic block capture.

theorem block_inter_free_edges_eq_vertex_filter {n : ℕ}
    (S : Finset (GraphEdge n)) (B : Finset (Fin n)) (u : Fin n)
    (h : B ∩ S.biUnion (fun e => e.val) = {u}) :
    S ∩ Finset.univ.filter (fun e : GraphEdge n => ¬Disjoint e.val B) =
      S.filter (fun e => u ∈ e.val) := by
…

Mentions: OAI.Problem313.GraphEdge

theorem OAI.Problem313.count_capturing_blocks_ge_singleton_inter line 76

Source documentation

Counting singleton-intersection blocks gives a lower bound for counting blocks that capture the support in the desired degree range.

theorem count_capturing_blocks_ge_singleton_inter {n : ℕ}
    (S : Finset (GraphEdge n)) (blocks : Finset (Finset (Fin n)))
    (u : Fin n) (k : ℝ)
    (hpos : 1 ≤ (S.filter (fun e => u ∈ e.val)).card)
    (hdeg : ((S.filter (fun e => u ∈ e.val)).card : ℝ) ≤ k) :
    (blocks.filter (fun B => B ∩ S.biUnion (fun e => e.val) = {u})).card ≤
      (blocks.filter (fun B =>
        1 ≤ (S.filter (fun e => (e.val ∩ B).Nonempty)).card ∧
        ((S.filter (fun e => (e.val ∩ B).Nonempty)).card : ℝ) ≤ k)).card := by
…

Mentions: OAI.Problem313.GraphEdge