RandomSelection.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.RandomSelection.bad_threshold_fraction_le line 11

Source documentation

A simultaneous variable-threshold Markov bound on the fraction of bad samples.

theorem bad_threshold_fraction_le {Ω J : Type*} [Fintype Ω] [Nonempty Ω]
    [DecidableEq Ω] (tests : Finset J) (score : Ω → J → ℝ)
    (threshold ε : J → ℝ)
    (hnonneg : ∀ ω, ∀ j ∈ tests, 0 ≤ score ω j)
    (hpos : ∀ j ∈ tests, 0 < threshold j)
    (hmean : ∀ j ∈ tests, (∑ ω, score ω j) ≤
      (Fintype.card Ω : ℝ) * ε j * threshold j) :
    ((Finset.univ.filter (fun ω => ∃ j ∈ tests, threshold j < score ω j)).card : ℝ) /
      Fintype.card Ω ≤ ∑ j ∈ tests, ε j := by
…

theorem OAI.Problem337.RandomSelection.exists_middle_thresholds_and_terminal_blocks line 55

Source documentation

A finite realization simultaneously meeting all middle-level mean thresholds and enjoying a successful block for every terminal integer.

theorem exists_middle_thresholds_and_terminal_blocks (δ : ℝ) (hδ : δ < 1) :
    ∃ N : ℕ, ∀ (Ω J : Type) [Fintype Ω] [Nonempty Ω]
      (tests : Finset J) (score : Ω → J → ℝ) (threshold ε : J → ℝ)
      (s : Finset ℕ) (B : ℕ → Finset Ω),
      (∀ ω, ∀ j ∈ tests, 0 ≤ score ω j) →
      (∀ j ∈ tests, 0 < threshold j) →
      (∀ j ∈ tests, (∑ ω, score ω j) ≤
        (Fintype.card Ω : ℝ) * ε j * threshold j) →
      (∑ j ∈ tests, ε j) ≤ δ →
      (∀ u ∈ s, N ≤ u) →
      (∀ u ∈ s, ((B u).card : ℝ) / Fintype.card Ω ≤
        (u : ℝ) ^ (-(1 / 200 : ℝ))) →
…