RoutingBudget.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Problem310.RoutingBudget.ennreal_card_mul_pow_lt line 11

Source documentation

Transfer a real finite-union estimate to the extended-nonnegative probability scale.

lemma ennreal_card_mul_pow_lt {p q : ℝ} (hp : 0 < p) (hq : 0 ≤ q)
    (N k : ℕ) (h : (N : ℝ) * q ^ k < p) :
    (N : ENNReal) * (ENNReal.ofReal q) ^ k < ENNReal.ofReal p := by
…

theorem OAI.Problem310.RoutingBudget.exists_nondefault_parameters line 21

Source documentation

Choose parameters in the router convention: M is the number of nondefault children, so there are M + 1 children altogether. The last estimate is ready for an ENNReal finite union bound over the monotone-key representatives.

theorem exists_nondefault_parameters (p : ℝ) (hp : 0 < p) (hp1 : p < 1) :
    ∃ M d R : ℕ, 1 ≤ M ∧ 1 ≤ d ∧ 1 ≤ R ∧
      10 ≤ p * (M : ℝ) / 2 ∧
      (1 - ((2 : ℝ)⁻¹) ^ M) ^ d < p ∧
      ∀ r : ℕ, R ≤ r → ∀ N : ℕ,
        N ≤ 1 + M * r * 2 ^ (2 * r + 2) →
        (N : ENNReal) * (ENNReal.ofReal (1 - p / 2)) ^ (M * r) <
          ENNReal.ofReal p := by
…

lemma OAI.Problem310.RoutingBudget.ennreal_survival_lt line 55
Source documentation
The real survival estimate has exactly the expected truncated-subtraction form for the product probability measure.
```
lemma ennreal_survival_lt {p : ℝ} (hp : 0 < p) (M d : ℕ)
    (h : (1 - ((2 : ℝ)⁻¹) ^ M) ^ d < p) :
    (1 - ((2 : ENNReal)⁻¹) ^ M) ^ d < ENNReal.ofReal p := by
…
```