GraphBlockCapture.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

The graph-combinatorial input to capture of low Fourier levels.

def OAI.Problem313.BlockDetects line 17
Source documentation
A block detects a support when the restricted Fourier degree is positive and no larger than the specified real cutoff.
```
def BlockDetects {n : ℕ} (k : ℝ) (S : Finset (GraphEdge n))
    (B : Finset (Fin n)) : Prop :=
…
```
Mentions: OAI.Problem313.GraphEdge
instance OAI.Problem313.blockDetects_decidable line 22

theorem OAI.Problem313.exists_vertex_singleton_implies_detection line 28

Source documentation

For a low-degree support, choose one positive-degree vertex whose isolation by the random block guarantees detection.

theorem exists_vertex_singleton_implies_detection {n : ℕ}
    (S : Finset (GraphEdge n)) (hS : S.Nonempty) {k : ℝ}
    (hk : 0 ≤ k) (hcard : (S.card : ℝ) ≤ k ^ 2 / 2) :
    ∃ u ∈ S.biUnion (fun e => e.val), ∀ B : Finset (Fin n),
      B ∩ S.biUnion (fun e => e.val) = {u} → BlockDetects k S B := by
…

Mentions: OAI.Problem313.GraphEdge, OAI.Problem313.BlockDetects

theorem OAI.Problem313.block_detection_probability_of_singleton line 42

Source documentation

Transfer any uniform singleton-intersection bound to a detection bound.

theorem block_detection_probability_of_singleton {n : ℕ}
    (blocks : Finset (Finset (Fin n))) (S : Finset (GraphEdge n))
    (hS : S.Nonempty) {k a : ℝ} (hk : 0 ≤ k)
    (hcard : (S.card : ℝ) ≤ k ^ 2 / 2)
    (hsingle : ∀ u ∈ S.biUnion (fun e => e.val),
      a ≤ ((blocks.filter (fun B => B ∩ S.biUnion (fun e => e.val) = {u})).card : ℝ) /
        blocks.card) :
    a ≤ ((blocks.filter (BlockDetects k S)).card : ℝ) / blocks.card := by
…

Mentions: OAI.Problem313.GraphEdge, OAI.Problem313.BlockDetects

theorem OAI.Problem313.support_singleton_error_le_half line 63

Source documentation

The support-vertex bound turns the random-block union-bound error into a uniform error at most one half.

theorem support_singleton_error_le_half {n : ℕ}
    (S : Finset (GraphEdge n)) (k r : ℝ)
    (hcard : (S.card : ℝ) ≤ k ^ 2 / 2)
    (hr : 0 ≤ r) (hbudget : k ^ 2 * r ≤ 1 / 2) :
    (((S.biUnion (fun e => e.val)).card : ℝ) - 1) * r ≤ 1 / 2 := by
…

Mentions: OAI.Problem313.GraphEdge

theorem OAI.Problem313.block_detection_probability_lower line 76

Source documentation

Quantitative detection from the singleton-intersection union bound. The scalar r will be (m-1)/(n-1) for a uniformly chosen m-vertex block.

theorem block_detection_probability_lower {n : ℕ}
    (blocks : Finset (Finset (Fin n))) (S : Finset (GraphEdge n))
    (hS : S.Nonempty) (k q r : ℝ) (hk : 0 ≤ k) (hq : 0 ≤ q)
    (hcard : (S.card : ℝ) ≤ k ^ 2 / 2) (hr : 0 ≤ r)
    (hbudget : k ^ 2 * r ≤ 1 / 2)
    (hsingle : ∀ u ∈ S.biUnion (fun e => e.val),
      q * (1 - (((S.biUnion (fun e => e.val)).card : ℝ) - 1) * r) ≤
        ((blocks.filter (fun B => B ∩ S.biUnion (fun e => e.val) = {u})).card : ℝ) /
          blocks.card) :
    q / 2 ≤ ((blocks.filter (BlockDetects k S)).card : ℝ) / blocks.card := by
…

Mentions: OAI.Problem313.GraphEdge, OAI.Problem313.BlockDetects

theorem OAI.Problem313.sqrt_block_cutoff_le_log line 95

Source documentation

The biased Fourier cutoff for a square-root block never exceeds log n.

theorem sqrt_block_cutoff_le_log (n : ℕ) (sigma : ℝ) (hn : 2 ≤ n)
    (ht : 16 ≤ Real.log (n : ℝ)) (hsigma : 0 ≤ sigma) (hsigma1 : sigma ≤ 1 / 2) :
    0 ≤ sigma * Real.log (⌊Real.sqrt (n : ℝ)⌋₊ : ℝ) / 64 ∧
      sigma * Real.log (⌊Real.sqrt (n : ℝ)⌋₊ : ℝ) / 64 ≤ Real.log (n : ℝ) := by
…

theorem OAI.Problem313.sqrt_block_cutoff_budget line 110

Source documentation

Uniform numerical budget used in detecting supports of at most k²/2 edges.

theorem sqrt_block_cutoff_budget (n : ℕ) (sigma : ℝ) (hn : 2 ≤ n)
    (ht : 16 ≤ Real.log (n : ℝ)) (hsigma : 0 ≤ sigma) (hsigma1 : sigma ≤ 1 / 2) :
    (sigma * Real.log (⌊Real.sqrt (n : ℝ)⌋₊ : ℝ) / 64) ^ 2 *
        (((⌊Real.sqrt (n : ℝ)⌋₊ : ℝ) - 1) / ((n : ℝ) - 1)) ≤ 1 / 2 := by
…

theorem OAI.Problem313.sqrt_block_detection_probability line 129

Source documentation

Every nonempty support of degree at most k²/2 is detected with probability at least m/(2*n) by the square-root-sized random block.

theorem sqrt_block_detection_probability (n : ℕ) (sigma : ℝ) (hn : 2 ≤ n)
    (ht : 16 ≤ Real.log (n : ℝ)) (hsigma : 0 ≤ sigma) (hsigma1 : sigma ≤ 1 / 2)
    (S : Finset (GraphEdge n)) (hS : S.Nonempty)
    (hcard : (S.card : ℝ) ≤
      (sigma * Real.log (⌊Real.sqrt (n : ℝ)⌋₊ : ℝ) / 64) ^ 2 / 2) :
    (⌊Real.sqrt (n : ℝ)⌋₊ : ℝ) / (2 * n) ≤
      blockProbability (Finset.univ : Finset (Fin n)) ⌊Real.sqrt (n : ℝ)⌋₊
        (BlockDetects (sigma * Real.log (⌊Real.sqrt (n : ℝ)⌋₊ : ℝ) / 64) S) := by
…

Mentions: OAI.Problem313.GraphEdge, OAI.Problem313.blockProbability, OAI.Problem313.BlockDetects

theorem OAI.Problem313.graph_block_detection_probability line 162

Source documentation

The graph-bias version, with the normalized cardinal ratio exposed for the finite averaging lemma. No restriction on p is needed for this combinatorics.

theorem graph_block_detection_probability (n : ℕ) (p : ℝ) (hn : 2 ≤ n)
    (ht : 16 ≤ Real.log (n : ℝ))
    (S : Finset (GraphEdge n)) (hS : S.Nonempty)
    (hcard : (S.card : ℝ) ≤
      (Real.sqrt (p * (1 - p)) * Real.log (⌊Real.sqrt (n : ℝ)⌋₊ : ℝ) / 64) ^ 2 / 2) :
    (⌊Real.sqrt (n : ℝ)⌋₊ : ℝ) / (2 * n) ≤
      ((((Finset.univ : Finset (Fin n)).powersetCard ⌊Real.sqrt (n : ℝ)⌋₊).filter
        (BlockDetects (Real.sqrt (p * (1 - p)) *
          Real.log (⌊Real.sqrt (n : ℝ)⌋₊ : ℝ) / 64) S)).card : ℝ) /
        ((Finset.univ : Finset (Fin n)).powersetCard ⌊Real.sqrt (n : ℝ)⌋₊).card := by
…

Mentions: OAI.Problem313.GraphEdge, OAI.Problem313.BlockDetects

theorem OAI.Problem313.blockDetects_iff_inter_free_edges line 181

Source documentation

An equivalent presentation using intersection with the finite free-edge set.

theorem blockDetects_iff_inter_free_edges {n : ℕ} (k : ℝ)
    (S : Finset (GraphEdge n)) (B : Finset (Fin n)) :
    BlockDetects k S B ↔
      1 ≤ (S ∩ Finset.univ.filter (fun e : GraphEdge n => ¬Disjoint e.val B)).card ∧
        ((S ∩ Finset.univ.filter (fun e : GraphEdge n => ¬Disjoint e.val B)).card : ℝ) ≤ k := by
…

Mentions: OAI.Problem313.GraphEdge, OAI.Problem313.BlockDetects