OAI/Combinatorics/SharpThreshold/SharpThreshold.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem313.graphQuantile_width_of_variance_bound line 14

   Source documentation

   The entire threshold-width deduction, with the variance estimate as its only additional quantitative hypothesis.

   theorem graphQuantile_width_of_variance_bound {n : ℕ} {f : GraphConfig n → Bool}
       {C ε : ℝ} (hC : 0 ≤ C)
       (hmono : IncreasingGraphProperty f) (hnt : NontrivialGraphProperty f)
       (hε : 0 < ε) (hεhalf : ε < (1 / 2 : ℝ))
       (hvariance : ∀ p ∈ Set.Ioo (0 : ℝ) 1,
         graphVariance p f ≤ C * totalInfluence p f) :
       graphQuantile (1 - ε) f - graphQuantile ε f ≤
         (4 * C) * Real.log (1 / (2 * ε)) := by
   …

   Mentions: OAI.Problem313.GraphConfig, OAI.Problem313.IncreasingGraphProperty, OAI.Problem313.NontrivialGraphProperty, OAI.Problem313.graphVariance, OAI.Problem313.totalInfluence, OAI.Problem313.graphQuantile

2. theorem OAI.Problem313.sharp_threshold_width_of_variance_bound line 52

   Source documentation

   The logarithmic-square threshold-width bound follows from the variance bound.

   theorem sharp_threshold_width_of_variance_bound
       (hvariance : ∀ (n : ℕ) (f : GraphConfig n → Bool) (p : ℝ),
         2 ≤ n → VertexInvariant f → 0 < p → p < 1 →
         graphVariance p f ≤ ((2 : ℝ) ^ 17 / (Real.log (n : ℝ)) ^ 2) *
           totalInfluence p f) :
       ∀ (n : ℕ) (f : GraphConfig n → Bool) (ε : ℝ),
         2 ≤ n → VertexInvariant f → IncreasingGraphProperty f →
         NontrivialGraphProperty f → 0 < ε → ε < (1 / 2 : ℝ) →
         graphQuantile (1 - ε) f - graphQuantile ε f ≤
           ((2 : ℝ) ^ 19 / (Real.log (n : ℝ)) ^ 2) *
             Real.log (1 / (2 * ε)) := by
   …

   Mentions: OAI.Problem313.GraphConfig, OAI.Problem313.VertexInvariant, OAI.Problem313.graphVariance, OAI.Problem313.totalInfluence, OAI.Problem313.IncreasingGraphProperty, OAI.Problem313.NontrivialGraphProperty, OAI.Problem313.graphQuantile