BlockSize.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem313.half_le_nat_floor line 9

theorem OAI.Problem313.sqrt_block_size_bounds line 15

Source documentation

Elementary size estimates for the square-root vertex block.

theorem sqrt_block_size_bounds (n : ℕ) (hn : 2 ≤ n)
    (ht : 16 ≤ Real.log (n : ℝ)) :
    3 ≤ ⌊Real.sqrt (n : ℝ)⌋₊ ∧
      ⌊Real.sqrt (n : ℝ)⌋₊ ≤ n ∧
      Real.sqrt (n : ℝ) / 2 ≤ (⌊Real.sqrt (n : ℝ)⌋₊ : ℝ) := by
…

theorem OAI.Problem313.log_sqrt_block_lower line 34

Source documentation

The square-root block retains at least one third of the original logarithm.

theorem log_sqrt_block_lower (n : ℕ) (hn : 2 ≤ n)
    (ht : 16 ≤ Real.log (n : ℝ)) :
    Real.log (n : ℝ) / 3 ≤ Real.log (⌊Real.sqrt (n : ℝ)⌋₊ : ℝ) := by
…

theorem OAI.Problem313.sqrt_block_pair_ratio line 49

Source documentation

Pair-inclusion correction for the square-root-sized uniform block.

theorem sqrt_block_pair_ratio (n : ℕ) (hn : 2 ≤ n) :
    ((⌊Real.sqrt (n : ℝ)⌋₊ : ℝ) - 1) / ((n : ℝ) - 1) ≤
      1 / Real.sqrt (n : ℝ) := by
…

theorem OAI.Problem313.block_capture_exp_lower line 64
Source documentation
A coarse exponential estimate sufficient for the block-capture union bound.
```
theorem block_capture_exp_lower (t : ℝ) (ht : 16 ≤ t) :
    2 * t ^ 2 ≤ Real.exp (t / 2) := by
…
```
theorem OAI.Problem313.block_capture_decay line 86
theorem OAI.Problem313.log_square_div_sqrt_le_half line 94

theorem OAI.Problem313.sqrt_block_capture_correction line 104

Source documentation

The numerical loss in the singleton-capture union bound is at most one half.

theorem sqrt_block_capture_correction (n : ℕ) (v : ℝ) (hn : 2 ≤ n)
    (ht : 16 ≤ Real.log (n : ℝ)) (hvone : 1 ≤ v)
    (hv : v ≤ (Real.log (n : ℝ)) ^ 2) :
    (v - 1) * (((⌊Real.sqrt (n : ℝ)⌋₊ : ℝ) - 1) / ((n : ℝ) - 1)) ≤
      (1 / 2 : ℝ) := by
…