OAI/Combinatorics/ProgressionColoring/OuterColoring.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.QuantitativeVanDerWaerden.outer_log_one_sub_lower line 16
2. theorem OAI.QuantitativeVanDerWaerden.outer_exp_neg_two_le_one_sub line 27
3. theorem OAI.QuantitativeVanDerWaerden.outer_exp_sum_le_product line 32
4. theorem OAI.QuantitativeVanDerWaerden.outer_local_criterion line 57

   Source documentation

   The numerical criterion used for each outer bad event.

   theorem outer_local_criterion {I : Type uI} (s : Finset I) (z : I → ℝ) (l : ℝ)
       (hl : 100 ≤ l) (hz : ∀ i ∈ s, 0 ≤ z i)
       (hzhalf : ∀ i ∈ s, z i ≤ 1 / 2)
       (hsum : ∑ i ∈ s, z i ≤ l / 500) :
       2 * Real.exp (-l / 8) ≤ Real.exp (-l / 32) * ∏ i ∈ s, (1 - z i) := by
   …

5. theorem OAI.QuantitativeVanDerWaerden.outer_weight_pos line 84
6. theorem OAI.QuantitativeVanDerWaerden.outer_weight_lt_half line 86
7. def OAI.QuantitativeVanDerWaerden.outerNeighbors line 99

   Source documentation

   Distinct tests are adjacent precisely when they share a label variable.

   noncomputable def outerNeighbors {I : Type uI} {Label : Type uLabel} [Fintype I] [DecidableEq I]
       [DecidableEq Label] (support : I → Finset Label) (i : I) : Finset I :=
   …

8. theorem OAI.QuantitativeVanDerWaerden.outer_neighbor_weight_bound line 104

   Source documentation

   A per-label incident bound gives the required per-test neighbor bound.

   theorem outer_neighbor_weight_bound {I : Type uI} {Label : Type uLabel} [Fintype I] [DecidableEq I]
       [DecidableEq Label] (support : I → Finset Label) (weight : I → ℝ)
       (hweight : ∀ i, 0 ≤ weight i) (B : ℝ)
       (hincident : ∀ b, ∑ j ∈ Finset.univ.filter (fun j => b ∈ support j), weight j ≤ B)
       (i : I) :
       ∑ j ∈ outerNeighbors support i, weight j ≤ (support i).card * B := by
   …

   Mentions: OAI.QuantitativeVanDerWaerden.outerNeighbors