SamplingAvoidance.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Avoiding a finite family of events by counting

The cardinality of a finite union is bounded by the sum of the individual cardinalities. A strict bound below the size of the ambient finite type therefore supplies an element outside every event. The rational corollary uses normalized cardinalities and requires no independence assumption.

theorem OAI.Problem348.Sampling.exists_avoiding_of_sum_card_lt line 23

Source documentation

A family of finite bad events whose summed cardinality is smaller than the ambient finite type has an element avoiding every event in the family.

theorem exists_avoiding_of_sum_card_lt {Ω : Type uOmega} {I : Type uI} [Fintype Ω]
    (events : Finset I) (bad : I → Finset Ω)
    (hsmall : (∑ i ∈ events, (bad i).card) < Fintype.card Ω) :
    ∃ ω, ∀ i ∈ events, ω ∉ bad i := by
…

theorem OAI.Problem348.Sampling.exists_avoiding_of_uniform_ratio_lt line 39

Source documentation

Uniform rational bounds on the normalized bad-event cardinalities give an avoiding element when the number of events times the bound is less than one. The events may overlap arbitrarily.

theorem exists_avoiding_of_uniform_ratio_lt {Ω : Type uOmega} {I : Type uI} [Fintype Ω]
    (events : Finset I) (bad : I → Finset Ω) (r : ℚ)
    (hΩ : 0 < Fintype.card Ω)
    (hbound : ∀ i ∈ events, ((bad i).card : ℚ) / (Fintype.card Ω : ℚ) ≤ r)
    (hsmall : (events.card : ℚ) * r < 1) :
    ∃ ω, ∀ i ∈ events, ω ∉ bad i := by
…

theorem OAI.Problem348.Sampling.exists_avoiding_of_card_mul_le line 62

Source documentation

A fraction-free uniform union bound. Every bad event occupies at most 1 / q of the finite sample space; fewer than q bad events can be avoided. No independence between the bad events is required.

theorem exists_avoiding_of_card_mul_le {Ω : Type uOmega} {I : Type uI} [Fintype Ω]
    (events : Finset I) (bad : I → Finset Ω) (q : ℕ)
    (hΩ : 0 < Fintype.card Ω)
    (hbound : ∀ i ∈ events, (bad i).card * q ≤ Fintype.card Ω)
    (hsmall : events.card < q) :
    ∃ ω, ∀ i ∈ events, ω ∉ bad i := by
…

theorem OAI.Problem348.Sampling.exists_selection_avoiding line 82

Source documentation

The cellwise counting form of sampling avoidance. The relation selected ω e means that sample ω uses the relevant cell e. The budget is the square of the common size of the axis classes.

theorem exists_selection_avoiding {Ω : Type uOmega} {Cell : Type uCell} [Fintype Ω]
    (changed : Finset Cell) (selected : Ω → Cell → Prop) (m : ℕ)
    [DecidableRel selected]
    (hΩ : 0 < Fintype.card Ω)
    (hbound : ∀ e ∈ changed,
      (Finset.univ.filter (fun ω => selected ω e)).card * m ^ 2 ≤ Fintype.card Ω)
    (hsmall : changed.card < m ^ 2) :
    ∃ ω, ∀ e ∈ changed, ¬ selected ω e := by
…

theorem OAI.Problem348.Sampling.exists_agreement_of_changed_card_lt line 96

Source documentation

Agreement on every protected selected cell follows from the cellwise sampling estimate. Unprotected cells are allowed to change arbitrarily.

theorem exists_agreement_of_changed_card_lt
    {Ω : Type uOmega} {Cell : Type uCell} {Value : Type uValue} [Fintype Ω] [Fintype Cell] [DecidableEq Value]
    (A B : Cell → Value) (selected : Ω → Cell → Prop)
    (relevant : Cell → Prop) [DecidableRel selected] [DecidablePred relevant]
    (m : ℕ) (hΩ : 0 < Fintype.card Ω)
    (hbound : ∀ e, relevant e →
      (Finset.univ.filter (fun ω => selected ω e)).card * m ^ 2 ≤ Fintype.card Ω)
    (hsmall : (Finset.univ.filter (fun e => A e ≠ B e)).card < m ^ 2) :
    ∃ ω, ∀ e, relevant e → selected ω e → A e = B e := by
…

theorem OAI.Problem348.Sampling.exists_agreement_three_seed line 119

Source documentation

Version for the three-seed sample space used in the tree construction. There are m³ samples, and a protected cell occurs in at most m of them.

theorem exists_agreement_three_seed
    {Cell : Type uCell} {Value : Type uValue} [Fintype Cell] [DecidableEq Value]
    (m : ℕ) (hm : 0 < m) (A B : Cell → Value)
    (selected : (Fin m × Fin m × Fin m) → Cell → Prop)
    (relevant : Cell → Prop) [DecidableRel selected] [DecidablePred relevant]
    (hbound : ∀ e, relevant e →
      (Finset.univ.filter (fun ω => selected ω e)).card ≤ m)
    (hsmall : (Finset.univ.filter (fun e => A e ≠ B e)).card < m ^ 2) :
    ∃ ω, ∀ e, relevant e → selected ω e → A e = B e := by
…

theorem OAI.Problem348.Sampling.sq_le_changed_card_of_forcing line 140

Source documentation

Contrapositive form: if every sample forces a changed protected cell, then at least m² entries have changed.

theorem sq_le_changed_card_of_forcing
    {Ω : Type uOmega} {Cell : Type uCell} {Value : Type uValue} [Fintype Ω] [Fintype Cell] [DecidableEq Value]
    (A B : Cell → Value) (selected : Ω → Cell → Prop)
    (relevant : Cell → Prop) [DecidableRel selected] [DecidablePred relevant]
    (m : ℕ) (hΩ : 0 < Fintype.card Ω)
    (hbound : ∀ e, relevant e →
      (Finset.univ.filter (fun ω => selected ω e)).card * m ^ 2 ≤ Fintype.card Ω)
    (hforcing : ∀ ω, ∃ e, relevant e ∧ selected ω e ∧ A e ≠ B e) :
    m ^ 2 ≤ (Finset.univ.filter (fun e => A e ≠ B e)).card := by
…