DirectionBudget.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The numerical budget for robust directions

The scalar expression in the finite union bound is strictly below one for a sufficiently large prime chosen after the other finite parameters.

theorem OAI.MetricEntropyDuality.direction_bad_event_bound_eq line 18

Source documentation

The union-bound expression after substituting w = 2 * D.

theorem direction_bad_event_bound_eq (D h : ℕ) (u p : ℝ) (hp : p ≠ 0) :
    p ^ D * u ^ (h * (2 * D)) * ((h : ℝ) / p) ^ (2 * D) =
      (((h : ℝ) ^ 2 * u ^ (2 * h)) / p) ^ D := by
…

theorem OAI.MetricEntropyDuality.direction_bad_event_bound_lt_one line 34
Source documentation
The last-prime threshold makes the actual counting bound strictly less than one. No positivity of h or u is needed for this scalar implication.
```
theorem direction_bad_event_bound_lt_one {D h u p : ℕ} (hD : 0 < D)
    (hp : h ^ 2 * u ^ (2 * h) < p) :
    (p : ℝ) ^ D * (u : ℝ) ^ (h * (2 * D)) *
        ((h : ℝ) / p) ^ (2 * D) < 1 := by
…
```