OAI/NumberTheory/EgyptianFractions/PrimeTripleExclusion.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.fixed_sum_bad_coordinate_card_le line 9

   Source documentation

   Two coordinates determine a triple of fixed sum.

   theorem fixed_sum_bad_coordinate_card_le
       {α : Type*} [DecidableEq α] (T : Finset α) (B U : Finset ℕ)
       (x y z : α → ℕ) (n : ℕ)
       (hsum : ∀ t ∈ T, x t + y t + z t = n)
       (hy : ∀ t ∈ T, y t ∈ U)
       (hinj : Function.Injective (fun t => (x t, y t, z t))) :
       (T.filter (fun t => x t ∈ B)).card ≤ B.card * U.card := by
   …

2. theorem OAI.Problem337.fixed_sum_bad_triples_card_le line 37

   Source documentation

   A union bound for exceptional coordinates of fixed-sum triples.

   theorem fixed_sum_bad_triples_card_le
       (T : Finset (ℕ × ℕ × ℕ)) (B U : Finset ℕ) (n : ℕ)
       (hsum : ∀ t ∈ T, t.1 + t.2.1 + t.2.2 = n)
       (hU : ∀ t ∈ T, t.1 ∈ U ∧ t.2.1 ∈ U ∧ t.2.2 ∈ U) :
       (T.filter (fun t => t.1 ∈ B ∨ t.2.1 ∈ B ∨ t.2.2 ∈ B)).card ≤
         3 * B.card * U.card := by
   …

3. theorem OAI.Problem337.exists_fixed_sum_triple_avoiding line 86

   Source documentation

   More triples than the exceptional union bound give a good triple.

   theorem exists_fixed_sum_triple_avoiding
       (T : Finset (ℕ × ℕ × ℕ)) (B U : Finset ℕ) (n : ℕ)
       (hsum : ∀ t ∈ T, t.1 + t.2.1 + t.2.2 = n)
       (hU : ∀ t ∈ T, t.1 ∈ U ∧ t.2.1 ∈ U ∧ t.2.2 ∈ U)
       (hmany : 3 * B.card * U.card < T.card) :
       ∃ t ∈ T, t.1 ∉ B ∧ t.2.1 ∉ B ∧ t.2.2 ∉ B := by
   …