OAI/Combinatorics/SharpThreshold/BlockParameters.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Problem313.block_scale_pos line 10
  2. lemma OAI.Problem313.block_scale_le_half line 14
  3. lemma OAI.Problem313.block_cutoff_pos line 21
  4. lemma OAI.Problem313.block_cutoff_le_log_div_128 line 30
  5. lemma OAI.Problem313.block_cutoff_le_log line 45
  6. lemma OAI.Problem313.log_sq_le_sixteen_sqrt line 53

    Source documentation

    A global logarithmic bound which avoids any large-parameter decay calculus.

    lemma log_sq_le_sixteen_sqrt (x : ℝ) (hx : 1 ≤ x) :
    (Real.log x) ^ 2 ≤ 16 * Real.sqrt x := by
…
  7. lemma OAI.Problem313.block_cutoff_sq_div_sqrt_le_half line 69

    Source documentation

    The support-size correction in the random block capture estimate.

    lemma block_cutoff_sq_div_sqrt_le_half (n : ℕ) (p : ℝ) (hn : 2 ≤ n)
    (ht : 16 ≤ Real.log (n : ℝ)) :
    (Real.sqrt (p * (1 - p)) *
      Real.log (⌊Real.sqrt (n : ℝ)⌋₊ : ℝ) / 64) ^ 2 /
        Real.sqrt (n : ℝ) ≤ 1 / 2 := by
…
  8. lemma OAI.Problem313.block_cutoff_sq_pair_ratio_le_half line 86

    Source documentation

    The exact pair-correction form needed by uniform block counting.

    lemma block_cutoff_sq_pair_ratio_le_half (n : ℕ) (p : ℝ) (hn : 2 ≤ n)
    (ht : 16 ≤ Real.log (n : ℝ)) :
    (Real.sqrt (p * (1 - p)) *
      Real.log (⌊Real.sqrt (n : ℝ)⌋₊ : ℝ) / 64) ^ 2 *
        (((⌊Real.sqrt (n : ℝ)⌋₊ : ℝ) - 1) / ((n : ℝ) - 1)) ≤ 1 / 2 := by
…
  9. lemma OAI.Problem313.block_support_pair_correction_le_half line 99
  10. theorem OAI.Problem313.graph_block_preconstant_bound line 116

    Source documentation

    The full numerical coefficient for the actual square-root block parameters.

    theorem graph_block_preconstant_bound (n : ℕ) (p : ℝ) (hn : 2 ≤ n)
    (ht : 16 ≤ Real.log (n : ℝ)) (hp : 0 < p) (hp1 : p < 1) :
    4 * (⌊Real.sqrt (n : ℝ)⌋₊ : ℝ) ^ (-(1 : ℝ) / 4) +
        2 * (Real.sqrt (p * (1 - p))) ^ 2 /
          (Real.sqrt (p * (1 - p)) *
            Real.log (⌊Real.sqrt (n : ℝ)⌋₊ : ℝ) / 64) ^ 2 ≤
      (2 : ℝ) ^ 17 / (Real.log (n : ℝ)) ^ 2 := by
…
  11. theorem OAI.Problem313.small_log_poincare_coefficient line 129

    Source documentation

    The elementary coefficient comparison in the small-logarithm branch.

    theorem small_log_poincare_coefficient (n : ℕ) (p : ℝ) (hn : 2 ≤ n)
    (ht : Real.log (n : ℝ) ≤ 16) :
    p * (1 - p) ≤ (2 : ℝ) ^ 17 / (Real.log (n : ℝ)) ^ 2 := by
…