LevelFailureMean.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.LevelFailureMean.sum_failure_counts line 11

Source documentation

Fubini for counts of failing integers at a level.

theorem sum_failure_counts {Ω U : Type*} [Fintype Ω] [DecidableEq Ω]
    (level : Finset U) (bad : Ω → U → Prop) [DecidableRel bad] :
    (∑ ω, ((level.filter (bad ω)).card : ℝ)) =
      ∑ u ∈ level, ((Finset.univ.filter (fun ω => bad ω u)).card : ℝ) := by
…

theorem OAI.Problem337.LevelFailureMean.level_failure_mean_le line 20

Source documentation

Pointwise failure probabilities bound the expected number of failing integers on a level, without any independence between integers.

theorem level_failure_mean_le {Ω U : Type*} [Fintype Ω] [Nonempty Ω]
    [DecidableEq Ω] (level : Finset U) (bad : Ω → U → Prop) [DecidableRel bad]
    (X e : ℝ) (he : 0 ≤ e) (hlevel : (level.card : ℝ) ≤ X)
    (hbad : ∀ u ∈ level,
      ((Finset.univ.filter (fun ω => bad ω u)).card : ℝ) / Fintype.card Ω ≤ e) :
    (∑ ω, ((level.filter (bad ω)).card : ℝ)) ≤
      (Fintype.card Ω : ℝ) * e * X := by
…

theorem OAI.Problem337.LevelFailureMean.middle_level_failure_mean_le line 41

Source documentation

The two middle-level exponential budgets differ by exactly exp(-m/250).

theorem middle_level_failure_mean_le {Ω U : Type*} [Fintype Ω] [Nonempty Ω]
    [DecidableEq Ω] (level : Finset U) (bad : Ω → U → Prop) [DecidableRel bad]
    (X m : ℝ) (hlevel : (level.card : ℝ) ≤ X)
    (hbad : ∀ u ∈ level,
      ((Finset.univ.filter (fun ω => bad ω u)).card : ℝ) / Fintype.card Ω ≤
        Real.exp (-m / 200)) :
    (∑ ω, ((level.filter (bad ω)).card : ℝ)) ≤ (Fintype.card Ω : ℝ) *
      Real.exp (-m / 250) * (X * Real.exp (-m / 1000)) := by
…

theorem OAI.Problem337.LevelFailureMean.middle_level_budget_le_half line 60
Source documentation
A deliberately coarse explicit onset suffices to absorb the number of levels.
```
theorem middle_level_budget_le_half (m : ℝ) (hm : 500000 ≤ m) :
    m * Real.exp (-m / 250) ≤ 1 / 2 := by
…
```

theorem OAI.Problem337.LevelFailureMean.exists_good_levels_and_terminal_blocks line 80

Source documentation

Concrete finite form of the simultaneous-selection step: one block has few failures at every middle level, while the collection of 1000 blocks succeeds at every sufficiently large terminal integer.

theorem exists_good_levels_and_terminal_blocks :
    ∃ N : ℕ, ∀ (Ω J : Type) [Fintype Ω] [Nonempty Ω]
      (tests : Finset J) (level : J → Finset ℕ) (X : J → ℝ) (m : ℝ)
      (middleBad terminalBad : Ω → ℕ → Prop)
      [DecidableRel middleBad] [DecidableRel terminalBad] (terminal : Finset ℕ),
      500000 ≤ m → (tests.card : ℝ) ≤ m →
      (∀ j ∈ tests, 0 < X j) →
      (∀ j ∈ tests, ((level j).card : ℝ) ≤ X j) →
      (∀ j ∈ tests, ∀ u ∈ level j,
        ((Finset.univ.filter (fun ω => middleBad ω u)).card : ℝ) /
          Fintype.card Ω ≤ Real.exp (-m / 200)) →
      (∀ u ∈ terminal, N ≤ u) →
…