OAI/Combinatorics/SharpThreshold/GraphBlockAverage.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem313.graph_fourier_capture_of_block_bounds line 22

   Source documentation

   The fixed-block Fourier estimate and the pointwise support-capture estimate combine into the global captured-mass bound. All graph sampling probabilities are the canonical blockProbability; the edge-touch bound is discharged here. The two hypotheses are precisely the analytic and combinatorial inputs, with no requirement that a single block capture every support simultaneously.

   theorem graph_fourier_capture_of_block_bounds
       {n m : ℕ} (f : GraphConfig n → Bool) {p : ℝ}
       (hp : 0 ≤ p) (hp1 : p ≤ 1) (hm : 1 ≤ m) (hmn : m ≤ n)
       (k a : ℝ) (ha : 0 ≤ a)
       (hcapture : ∀ S : Finset (GraphEdge n), S.Nonempty →
         (S.card : ℝ) ≤ k ^ 2 / 2 →
         (m : ℝ) / (2 * n) ≤
           blockProbability (Finset.univ : Finset (Fin n)) m (fun B =>
             1 ≤ (S.filter (EdgeTouches B)).card ∧
               ((S.filter (EdgeTouches B)).card : ℝ) ≤ k))
       (hblock : ∀ B : Finset (Fin n), B.card = m →
         (∑ S : Finset (GraphEdge n),
   …

   Mentions: OAI.Problem313.GraphConfig, OAI.Problem313.GraphEdge, OAI.Problem313.blockProbability, OAI.Problem313.EdgeTouches

2. theorem OAI.Problem313.graph_fourier_captured_mass_of_block_bound line 94

   Source documentation

   At the square-root block size all counting and numerical capture premises are discharged. Only the fixed-block analytic estimate remains as input.

   theorem graph_fourier_captured_mass_of_block_bound
       {n : ℕ} (f : GraphConfig n → Bool) {p : ℝ}
       (hn : 2 ≤ n) (ht : 16 ≤ Real.log (n : ℝ))
       (hp : 0 < p) (hp1 : p < 1)
       (hblock : ∀ B : Finset (Fin n), B.card = ⌊Real.sqrt (n : ℝ)⌋₊ →
         (∑ S : Finset (GraphEdge n),
           if 1 ≤ (S.filter (EdgeTouches B)).card ∧
               ((S.filter (EdgeTouches B)).card : ℝ) ≤
                 Real.sqrt (p * (1 - p)) * Real.log (⌊Real.sqrt (n : ℝ)⌋₊ : ℝ) / 64
           then BiasedFourier.coeff p (fun x => boolReal (f x)) S ^ 2 else 0) ≤
         (⌊Real.sqrt (n : ℝ)⌋₊ : ℝ) ^ (-1 / 4 : ℝ) *
           ∑ e : GraphEdge n, if EdgeTouches B e then edgeInfluence p f e else 0) :
   …

   Mentions: OAI.Problem313.GraphConfig, OAI.Problem313.GraphEdge, OAI.Problem313.EdgeTouches, OAI.Problem313.BiasedFourier.coeff, OAI.Problem313.boolReal, OAI.Problem313.edgeInfluence

3. theorem OAI.Problem313.graph_fourier_captured_mass line 132

   Source documentation

   The complete captured Fourier-mass bound for a vertex-invariant graph property. The bias is unrestricted within (0,1) and no monotonicity is used.

   theorem graph_fourier_captured_mass
       {n : ℕ} (f : GraphConfig n → Bool) {p : ℝ}
       (hn : 2 ≤ n) (ht : 16 ≤ Real.log (n : ℝ)) (hf : VertexInvariant f)
       (hp : 0 < p) (hp1 : p < 1) :
       (∑ S : Finset (GraphEdge n),
         if S.Nonempty ∧ (S.card : ℝ) ≤
             (Real.sqrt (p * (1 - p)) * Real.log (⌊Real.sqrt (n : ℝ)⌋₊ : ℝ) / 64) ^ 2 / 2
         then BiasedFourier.coeff p (fun x => boolReal (f x)) S ^ 2 else 0) ≤
         4 * (⌊Real.sqrt (n : ℝ)⌋₊ : ℝ) ^ (-1 / 4 : ℝ) * totalInfluence p f := by
   …

   Mentions: OAI.Problem313.GraphConfig, OAI.Problem313.VertexInvariant, OAI.Problem313.GraphEdge, OAI.Problem313.BiasedFourier.coeff, OAI.Problem313.boolReal, OAI.Problem313.totalInfluence