GraphVarianceBound.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem313.graphVariance_bound_of_spectral_inputs line 17

Source documentation

The graph-level variance reduction, with the two spectral identities and large-scale block capture supplied explicitly. No symmetry is needed after these inputs have been obtained.

theorem graphVariance_bound_of_spectral_inputs {n : ℕ}
    (f : GraphConfig n → Bool) (p : ℝ) (hn : 2 ≤ n) (hp : 0 < p) (hp1 : p < 1)
    (hvariance : graphVariance p f =
      ∑ S : Finset (GraphEdge n) with S.Nonempty,
        BiasedFourier.coeff p (fun x => boolReal (f x)) S ^ 2)
    (hdirichlet : (∑ S : Finset (GraphEdge n), (S.card : ℝ) *
        BiasedFourier.coeff p (fun x => boolReal (f x)) S ^ 2) =
      p * (1 - p) * totalInfluence p f)
    (hcapture : 16 ≤ Real.log (n : ℝ) →
      (∑ S : Finset (GraphEdge n) with S.Nonempty ∧
          (S.card : ℝ) ≤ (Real.sqrt (p * (1 - p)) *
            Real.log (⌊Real.sqrt (n : ℝ)⌋₊ : ℝ) / 64) ^ 2 / 2,
…

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

theorem OAI.Problem313.graphVariance_bound_of_dirichlet_capture line 53

Source documentation

Parseval discharges the variance identity, leaving the Dirichlet and captured-mass inputs.

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

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

theorem OAI.Problem313.graphVariance_bound_of_capture line 71

Source documentation

All spectral and numerical ingredients are discharged; only the graph-specific large-scale captured-mass estimate remains.

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

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

theorem OAI.Problem313.variance_influence_bound_core line 86
Source documentation
The graph variance bound, with all spectral, analytic, counting, and numerical inputs discharged.
```
theorem variance_influence_bound_core
    (n : ℕ) (f : GraphConfig n → Bool) (p : ℝ)
    (hn : 2 ≤ n) (hf : VertexInvariant f) (hp : 0 < p) (hp1 : p < 1) :
    graphVariance p f ≤
      ((2 : ℝ) ^ 17 / (Real.log (n : ℝ)) ^ 2) * totalInfluence p f := by
…
```
Mentions: OAI.Problem313.GraphConfig, OAI.Problem313.VertexInvariant, OAI.Problem313.graphVariance, OAI.Problem313.totalInfluence