RandomSelectionParameters.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.RandomProducts.eventually_blockLength_ge_log_mul line 12
Source documentation
floor(S/log S) eventually exceeds every fixed multiple of log S.
```
theorem eventually_blockLength_ge_log_mul (C : ℝ) :
    ∀ᶠ S : ℝ in atTop, C * Real.log S ≤ (blockLength S : ℝ) := by
…
```
Mentions: OAI.Problem337.RandomProducts.blockLength
theorem OAI.Problem337.RandomProducts.tendsto_blockLength_div_log_atTop line 31
theorem OAI.Problem337.RandomProducts.tendsto_blockLength_real_atTop line 39
theorem OAI.Problem337.RandomProducts.tendsto_middle_failure_zero line 46
Source documentation
The union over O(log S) middle levels has vanishing failure mass.
```
theorem tendsto_middle_failure_zero (K : ℝ) (hK : 0 ≤ K) :
    Tendsto (fun S : ℝ => K * Real.log S * Real.exp (-(blockLength S : ℝ) / 250))
      atTop (𝓝 0) := by
…
```
Mentions: OAI.Problem337.RandomProducts.blockLength
theorem OAI.Problem337.RandomProducts.eventually_middle_lower_cutoff line 75
Source documentation
Uniform lower cutoff for all middle-level numerators.
```
theorem eventually_middle_lower_cutoff :
    ∀ᶠ S : ℝ in atTop, ∀ V : ℝ,
      (9999 / 10000 : ℝ) * (blockLength S : ℝ) ≤ V →
      100000 * Real.log S ≤ V := by
…
```
Mentions: OAI.Problem337.RandomProducts.blockLength
theorem OAI.Problem337.RandomProducts.middle_frequency_cutoff line 87
Source documentation
Frequencies used by the middle-level discrepancy test lie within the range covered by the random second moment.
```
theorem middle_frequency_cutoff {m V : ℝ} (hm : 0 ≤ m)
    (hV : (9999 / 10000 : ℝ) * m ≤ V) :
    Real.exp (m / 2500) ≤ Real.exp (min m V / 200) := by
…
```

theorem OAI.Problem337.RandomProducts.middle_fourier_failure_bound line 96

Source documentation

One frequency union bound and Markov's inequality at the middle levels.

theorem middle_fourier_failure_bound {m w : ℝ} (hm : 0 ≤ m)
    (hw : (9999 / 10000 : ℝ) * m ≤ w) :
    Real.exp (m / 2500) * Real.exp (3 * m / 5000) * Real.exp (-w / 100) ≤
      Real.exp (-m / 200) := by
…

theorem OAI.Problem337.RandomProducts.middle_second_markov_factor line 105
Source documentation
The second Markov step has exactly the exponent used in the level union.
```
theorem middle_second_markov_factor (m : ℝ) :
    Real.exp (-m / 200) / Real.exp (-m / 1000) = Real.exp (-m / 250) := by
…
```

theorem OAI.Problem337.RandomProducts.terminal_fourier_failure_bound line 112

Source documentation

The corresponding first-block bound for terminal numerators.

theorem terminal_fourier_failure_bound {V : ℝ} (hV : 0 ≤ V) :
    Real.exp (V / 2500) * Real.exp (3 * V / 5000) * Real.exp (-V / 100) ≤
      Real.exp (-V / 200) := by
…

theorem OAI.Problem337.RandomProducts.terminal_thousand_blocks_bound line 121
Source documentation
Independence of 1000 terminal blocks converts the single-block estimate into a summable fifth-power tail.
```
theorem terminal_thousand_blocks_bound {V p : ℝ} (hp : 0 ≤ p)
    (hbound : p ≤ Real.exp (-V / 200)) :
    p ^ 1000 ≤ Real.exp (-5 * V) := by
…
```