OAI/NumberTheory/EgyptianFractions/IndependentBlockSelection.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.IndependentBlockSelection.card_all_bad_vectors line 10

   Source documentation

   Number of block choices in which every block belongs to one bad set.

   theorem card_all_bad_vectors {Ω : Type*} [Fintype Ω] [DecidableEq Ω]
       (B : Finset Ω) (R : ℕ) :
       (Finset.univ.filter (fun f : Fin R → Ω => ∀ i, f i ∈ B)).card = B.card ^ R := by
   …

2. theorem OAI.Problem337.IndependentBlockSelection.exists_blocks_of_bad_card_sum_lt line 25

   Source documentation

   A finite independent-block union bound with an explicit successful outcome. No probability or independence hypothesis is hidden: the sample space is exactly the Cartesian power Fin R → Ω.

   theorem exists_blocks_of_bad_card_sum_lt {Ω U : Type*} [Fintype Ω]
       (s : Finset U) (B : U → Finset Ω) (R : ℕ)
       (hsmall : (∑ u ∈ s, (B u).card ^ R) < Fintype.card Ω ^ R) :
       ∃ f : Fin R → Ω, ∀ u ∈ s, ∃ i : Fin R, f i ∉ B u := by
   …

3. theorem OAI.Problem337.IndependentBlockSelection.exists_blocks_of_probability_sum_lt line 50

   Source documentation

   Real-valued probability form, allowing distinct error budgets for each item.

   theorem exists_blocks_of_probability_sum_lt {Ω U : Type*} [Fintype Ω] [Nonempty Ω]
       (s : Finset U) (B : U → Finset Ω) (R : ℕ) (p : U → ℝ)
       (hbad : ∀ u ∈ s, ((B u).card : ℝ) / Fintype.card Ω ≤ p u)
       (hsmall : (∑ u ∈ s, p u ^ R) < 1) :
       ∃ f : Fin R → Ω, ∀ u ∈ s, ∃ i : Fin R, f i ∉ B u := by
   …

4. theorem OAI.Problem337.IndependentBlockSelection.finite_tail_sum_lt_of_summable line 75

   Source documentation

   Summability gives a uniform bound for every finite set beyond one cutoff.

   theorem finite_tail_sum_lt_of_summable (f : ℕ → ℝ) (hf : Summable f)
       {ε : ℝ} (hε : 0 < ε) :
       ∃ N : ℕ, ∀ s : Finset ℕ, (∀ u ∈ s, N ≤ u) → (∑ u ∈ s, f u) < ε := by
   …

5. theorem OAI.Problem337.IndependentBlockSelection.finite_inverse_fifth_tail_lt line 89

   Source documentation

   The terminal error u⁻⁵ is uniformly summable over arbitrary finite ranges.

   theorem finite_inverse_fifth_tail_lt {ε : ℝ} (hε : 0 < ε) :
       ∃ N : ℕ, ∀ s : Finset ℕ, (∀ u ∈ s, N ≤ u) →
         (∑ u ∈ s, (1 : ℝ) / (u : ℝ) ^ 5) < ε := by
   …

6. theorem OAI.Problem337.IndependentBlockSelection.exists_terminal_blocks line 96

   Source documentation

   Uniform terminal-level selection from an inverse-fifth-power block error.

   theorem exists_terminal_blocks :
       ∃ N : ℕ, ∀ (Ω : Type) [Fintype Ω] [Nonempty Ω]
         (s : Finset ℕ) (B : ℕ → Finset Ω) (R : ℕ) (p : ℕ → ℝ),
         (∀ u ∈ s, N ≤ u) →
         (∀ u ∈ s, ((B u).card : ℝ) / Fintype.card Ω ≤ p u) →
         (∀ u ∈ s, p u ^ R ≤ (1 : ℝ) / (u : ℝ) ^ 5) →
         ∃ f : Fin R → Ω, ∀ u ∈ s, ∃ i : Fin R, f i ∉ B u := by
   …

7. theorem OAI.Problem337.IndependentBlockSelection.exists_blocks_avoiding_global_bad_of_card_sum_lt line 110

   Source documentation

   Joint selection avoiding a global exceptional event and all local failures.

   theorem exists_blocks_avoiding_global_bad_of_card_sum_lt
       {Ω U : Type*} [Fintype Ω] (s : Finset U) (B : U → Finset Ω)
       (R : ℕ) (E : Finset (Fin R → Ω))
       (hsmall : E.card + (∑ u ∈ s, (B u).card ^ R) < Fintype.card Ω ^ R) :
       ∃ f : Fin R → Ω, f ∉ E ∧ ∀ u ∈ s, ∃ i : Fin R, f i ∉ B u := by
   …

8. theorem OAI.Problem337.IndependentBlockSelection.exists_blocks_avoiding_global_bad_of_probability_sum_lt line 143

   Source documentation

   Probability budgets add even when the global event is not independent of any of the individual terminal events.

   theorem exists_blocks_avoiding_global_bad_of_probability_sum_lt
       {Ω U : Type*} [Fintype Ω] [Nonempty Ω] (s : Finset U)
       (B : U → Finset Ω) (R : ℕ) (E : Finset (Fin R → Ω)) (p : U → ℝ)
       (hbad : ∀ u ∈ s, ((B u).card : ℝ) / Fintype.card Ω ≤ p u)
       (hsmall : (E.card : ℝ) / (Fintype.card Ω : ℝ) ^ R +
         (∑ u ∈ s, p u ^ R) < 1) :
       ∃ f : Fin R → Ω, f ∉ E ∧ ∀ u ∈ s, ∃ i : Fin R, f i ∉ B u := by
   …

9. theorem OAI.Problem337.IndependentBlockSelection.exists_terminal_blocks_with_global_bad line 172

   Source documentation

   Final simultaneous-selection form: a global budget below one leaves room for every sufficiently far-out finite collection of terminal integers.

   theorem exists_terminal_blocks_with_global_bad (δ : ℝ) (hδ : δ < 1) :
       ∃ N : ℕ, ∀ (Ω : Type) [Fintype Ω] [Nonempty Ω]
         (s : Finset ℕ) (B : ℕ → Finset Ω) (R : ℕ)
         (E : Finset (Fin R → Ω)) (p : ℕ → ℝ),
         (∀ u ∈ s, N ≤ u) →
         ((E.card : ℝ) / (Fintype.card Ω : ℝ) ^ R ≤ δ) →
         (∀ u ∈ s, ((B u).card : ℝ) / Fintype.card Ω ≤ p u) →
         (∀ u ∈ s, p u ^ R ≤ (1 : ℝ) / (u : ℝ) ^ 5) →
         ∃ f : Fin R → Ω, f ∉ E ∧ ∀ u ∈ s, ∃ i : Fin R, f i ∉ B u := by
   …

10. theorem OAI.Problem337.IndependentBlockSelection.thousand_blocks_rpow line 190

    Source documentation

    One thousand blocks turn u^(-.005) into the summable error u^(-5).

    theorem thousand_blocks_rpow (u : ℕ) :
        ((u : ℝ) ^ (-(1 / 200 : ℝ))) ^ 1000 = (1 : ℝ) / (u : ℝ) ^ 5 := by
    …

11. theorem OAI.Problem337.IndependentBlockSelection.exists_thousand_terminal_blocks_with_global_bad line 196

    Source documentation

    Explicit 1000-block form of simultaneous terminal selection.

    theorem exists_thousand_terminal_blocks_with_global_bad (δ : ℝ) (hδ : δ < 1) :
        ∃ N : ℕ, ∀ (Ω : Type) [Fintype Ω] [Nonempty Ω]
          (s : Finset ℕ) (B : ℕ → Finset Ω) (E : Finset (Fin 1000 → Ω)),
          (∀ u ∈ s, N ≤ u) →
          ((E.card : ℝ) / (Fintype.card Ω : ℝ) ^ 1000 ≤ δ) →
          (∀ u ∈ s, ((B u).card : ℝ) / Fintype.card Ω ≤
            (u : ℝ) ^ (-(1 / 200 : ℝ))) →
          ∃ f : Fin 1000 → Ω, f ∉ E ∧ ∀ u ∈ s, ∃ i : Fin 1000, f i ∉ B u := by
    …

12. theorem OAI.Problem337.IndependentBlockSelection.card_bad_first_block line 211

    Source documentation

    Restricting the first block has exactly its single-block failure fraction.

    theorem card_bad_first_block {Ω : Type*} [Fintype Ω] [DecidableEq Ω]
        (B : Finset Ω) (R : ℕ) :
        (Finset.univ.filter (fun f : Fin (R + 1) → Ω => f 0 ∈ B)).card =
          B.card * Fintype.card Ω ^ R := by
    …

13. theorem OAI.Problem337.IndependentBlockSelection.bad_first_block_fraction line 237

    Source documentation

    Normalized first-block bad count, for combining a middle-level event on block zero with terminal success on at least one of all blocks.

    theorem bad_first_block_fraction {Ω : Type*} [Fintype Ω] [Nonempty Ω] [DecidableEq Ω]
        (B : Finset Ω) (R : ℕ) :
        ((Finset.univ.filter (fun f : Fin (R + 1) → Ω => f 0 ∈ B)).card : ℝ) /
            (Fintype.card Ω : ℝ) ^ (R + 1) = (B.card : ℝ) / Fintype.card Ω := by
    …

14. theorem OAI.Problem337.IndependentBlockSelection.exists_middle_and_terminal_blocks line 250

    Source documentation

    A realization with a good middle-level block and a successful block for every terminal integer, matching the final simultaneous selection step.

    theorem exists_middle_and_terminal_blocks (δ : ℝ) (hδ : δ < 1) :
        ∃ N : ℕ, ∀ (Ω : Type) [Fintype Ω] [Nonempty Ω]
          (s : Finset ℕ) (B : ℕ → Finset Ω) (middleBad : Finset Ω),
          (∀ u ∈ s, N ≤ u) →
          ((middleBad.card : ℝ) / Fintype.card Ω ≤ δ) →
          (∀ u ∈ s, ((B u).card : ℝ) / Fintype.card Ω ≤
            (u : ℝ) ^ (-(1 / 200 : ℝ))) →
          ∃ f : Fin 1000 → Ω, f 0 ∉ middleBad ∧
            ∀ u ∈ s, ∃ i : Fin 1000, f i ∉ B u := by
    …