WindowBudgets.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Problem310.WindowBudget.tendsto_nat_mul_exp_neg line 13
Source documentation
A polynomial factor times a decaying exponential tends to zero along natural arguments.
```
lemma tendsto_nat_mul_exp_neg (a : ℝ) (ha : 0 < a) :
    Tendsto (fun r : ℕ => (r : ℝ) * Real.exp (-a * (r : ℝ))) atTop (𝓝 0) := by
…
```
lemma OAI.Problem310.WindowBudget.entropy_tendsto_zero line 21
Source documentation
The entropy factor appearing in the finite scale discretization is dominated by its exponential saving. This uses exactly the numerical coefficient.
```
lemma entropy_tendsto_zero (M a : ℝ) (ha : 10 ≤ a) :
    Tendsto (fun r : ℕ => 20 * M * (r : ℝ) * (1 + (2 : ℝ) ^ (2 * r + 2)) *
      Real.exp (-a * (r : ℝ))) atTop (𝓝 0) := by
…
```

lemma OAI.Problem310.WindowBudget.exists_entropy_threshold line 58

Source documentation

A single lower bound on the window length works for every larger window.

lemma exists_entropy_threshold (p M a : ℝ) (hp : 0 < p) (ha : 10 ≤ a) :
    ∃ r₀ : ℕ, 1 ≤ r₀ ∧ ∀ r : ℕ, r₀ ≤ r →
      20 * M * (r : ℝ) * (1 + (2 : ℝ) ^ (2 * r + 2)) *
        Real.exp (-a * (r : ℝ)) < p := by
…

lemma OAI.Problem310.WindowBudget.exists_branching_number line 69
Source documentation
Choose the branching number with the required exponential margin.
```
lemma exists_branching_number (p : ℝ) (hp : 0 < p) :
    ∃ M : ℕ, 2 ≤ M ∧ 10 ≤ p * ((M : ℝ) - 1) / 2 := by
…
```
lemma OAI.Problem310.WindowBudget.exists_positive_depth line 78
Source documentation
A geometric probability can be made arbitrarily small at a positive depth.
```
lemma exists_positive_depth (p q : ℝ) (hp : 0 < p) (hq0 : 0 ≤ q) (hq1 : q < 1) :
    ∃ d : ℕ, 1 ≤ d ∧ q ^ d < p := by
…
```

lemma OAI.Problem310.WindowBudget.exists_tree_parameters line 85

Source documentation

The branching factor and tree depth can be chosen in the prescribed order.

lemma exists_tree_parameters (p : ℝ) (hp : 0 < p) :
    ∃ M d : ℕ, 2 ≤ M ∧ 1 ≤ d ∧
      10 ≤ p * ((M : ℝ) - 1) / 2 ∧
      (1 - ((2 : ℝ)⁻¹) ^ (M - 1)) ^ d < p := by
…

lemma OAI.Problem310.WindowBudget.exists_gap line 99
Source documentation
Choose a gap after the finite tree has been fixed. The expression is K 2^(2-g) written without subtraction in a natural-number exponent.
```
lemma exists_gap (p : ℝ) (hp : 0 < p) (K : ℕ) :
    ∃ g : ℕ, 1 ≤ g ∧ (K : ℝ) * 4 * ((2 : ℝ)⁻¹) ^ g < p := by
…
```
lemma OAI.Problem310.WindowBudget.one_sub_pow_le_exp line 110
Source documentation
The elementary Bernoulli miss probability is bounded by an exponential.
```
lemma one_sub_pow_le_exp (u : ℝ) (hu : u ≤ 1) (N : ℕ) :
    (1 - u) ^ N ≤ Real.exp (-u * (N : ℝ)) := by
…
```

lemma OAI.Problem310.WindowBudget.exists_probability_threshold line 125

Source documentation

The window threshold also bounds the actual fixed-scale failure probability multiplied by the number of scale representatives.

lemma exists_probability_threshold (p : ℝ) (hp : 0 < p) (hp1 : p < 1)
    (M : ℕ) (hM : 2 ≤ M) (hmargin : 10 ≤ p * ((M : ℝ) - 1) / 2) :
    ∃ r₀ : ℕ, 1 ≤ r₀ ∧ ∀ r : ℕ, r₀ ≤ r →
      20 * (M : ℝ) * (r : ℝ) * (1 + (2 : ℝ) ^ (2 * r + 2)) *
        (1 - p / 2) ^ ((M - 1) * r) < p := by
…