SimultaneousSelection.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.card_exists_large_score_mul_le line 11

Source documentation

A finite Markov inequality with a union over frequencies. No independence between the frequencies, or between the points, is required.

theorem card_exists_large_score_mul_le {α β : Type*}
    (U : Finset α) (L : Finset β) (g : α → β → ℝ) (a : ℝ)
    (hg : ∀ u ∈ U, ∀ l ∈ L, 0 ≤ g u l) :
    ((U.filter (fun u => ∃ l ∈ L, a < g u l)).card : ℝ) * a ≤
      ∑ l ∈ L, ∑ u ∈ U, g u l := by
…

theorem OAI.Problem337.card_exists_large_norm_sq_mul_le line 33

Source documentation

Squared complex Fourier scores are a common instance of the preceding finite Markov/union estimate.

theorem card_exists_large_norm_sq_mul_le {α β : Type*}
    (U : Finset α) (L : Finset β) (f : α → β → ℂ) (a : ℝ) (ha : 0 ≤ a) :
    ((U.filter (fun u => ∃ l ∈ L, a < ‖f u l‖)).card : ℝ) * a ^ 2 ≤
      ∑ l ∈ L, ∑ u ∈ U, ‖f u l‖ ^ 2 := by
…

theorem OAI.Problem337.exists_simultaneous_below_thresholds line 57

Source documentation

A finite probabilistic-method selection principle. A normalized total expectation below one gives one sample satisfying all the thresholds.

theorem exists_simultaneous_below_thresholds {Ω J : Type*}
    (samples : Finset Ω) (tests : Finset J)
    (score : Ω → J → ℝ) (threshold : J → ℝ)
    (hnonneg : ∀ ω ∈ samples, ∀ j ∈ tests, 0 ≤ score ω j)
    (hpos : ∀ j ∈ tests, 0 < threshold j)
    (hbudget : (∑ j ∈ tests, (∑ ω ∈ samples, score ω j) / threshold j) <
      (samples.card : ℝ)) :
    ∃ ω ∈ samples, ∀ j ∈ tests, score ω j < threshold j := by
…

theorem OAI.Problem337.exists_simultaneous_of_mean_bounds line 86

Source documentation

Convenient per-test mean bounds for simultaneous selection.

theorem exists_simultaneous_of_mean_bounds {Ω J : Type*}
    (samples : Finset Ω) (tests : Finset J) (hsamples : samples.Nonempty)
    (score : Ω → J → ℝ) (threshold ε : J → ℝ)
    (hnonneg : ∀ ω ∈ samples, ∀ j ∈ tests, 0 ≤ score ω j)
    (hpos : ∀ j ∈ tests, 0 < threshold j)
    (hmean : ∀ j ∈ tests,
      (∑ ω ∈ samples, score ω j) ≤ (samples.card : ℝ) * ε j * threshold j)
    (hε : (∑ j ∈ tests, ε j) < 1) :
    ∃ ω ∈ samples, ∀ j ∈ tests, score ω j < threshold j := by
…

theorem OAI.Problem337.card_exists_large_norm_le_of_moments line 108

Source documentation

The uniform second-moment version of the frequency-union bound.

theorem card_exists_large_norm_le_of_moments {α β : Type*}
    (U : Finset α) (L : Finset β) (f : α → β → ℂ) (a E : ℝ)
    (ha : 0 < a) (hE : ∀ l ∈ L, (∑ u ∈ U, ‖f u l‖ ^ 2) ≤ E) :
    ((U.filter (fun u => ∃ l ∈ L, a < ‖f u l‖)).card : ℝ) ≤
      (L.card : ℝ) * E / a ^ 2 := by
…

theorem OAI.Problem337.exists_product_sample_avoiding line 126
Source documentation
A finite product-space union bound. Each test fails only if every coordinate belongs to its corresponding bad set. Different tests need not be independent. Allowed coordinate sets may be different, so one coordinate can simultaneously enforce a separate collection of middle-level tests.
```
theorem exists_product_sample_avoiding {ι Ω J : Type*} [Fintype ι]
    (allowed : ι → Finset Ω) (tests : Finset J) (bad : J → ι → Finset Ω)
    (hbudget : (∑ j ∈ tests, ∏ i, (bad j i).card) < ∏ i, (allowed i).card) :
    ∃ sample : ι → Ω, (∀ i, sample i ∈ allowed i) ∧
      ∀ j ∈ tests, ∃ i, sample i ∉ bad j i := by
…
```

theorem OAI.Problem337.exists_repeated_samples_avoiding line 148

Source documentation

Independent repetitions amplify a per-test failure cardinality to its R-th power. This is the terminal-block selection step in finite form.

theorem exists_repeated_samples_avoiding {Ω J : Type*}
    (samples : Finset Ω) (tests : Finset J) (bad : J → Finset Ω) (R : ℕ)
    (hbudget : (∑ j ∈ tests, (bad j).card ^ R) < samples.card ^ R) :
    ∃ sample : Fin R → Ω, (∀ i, sample i ∈ samples) ∧
      ∀ j ∈ tests, ∃ i, sample i ∉ bad j := by
…