OAI/Combinatorics/ProgressionColoring/FiniteLocalLemma.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.QuantitativeVanDerWaerden.FiniteLocalLemma.avoid line 18

   Source documentation

   Outcomes avoiding every bad event indexed by T.

   noncomputable def avoid (bad : I → Finset Ω) (T : Finset I) : Finset Ω := by
   …

2. theorem OAI.QuantitativeVanDerWaerden.FiniteLocalLemma.mem_avoid line 22
3. theorem OAI.QuantitativeVanDerWaerden.FiniteLocalLemma.avoid_empty line 29
4. theorem OAI.QuantitativeVanDerWaerden.FiniteLocalLemma.avoid_insert line 35
5. theorem OAI.QuantitativeVanDerWaerden.FiniteLocalLemma.avoid_antitone line 41
6. theorem OAI.QuantitativeVanDerWaerden.FiniteLocalLemma.avoid_mass_split line 47
7. theorem OAI.QuantitativeVanDerWaerden.FiniteLocalLemma.prod_antitone_of_unitInterval line 54

   Source documentation

   Products of factors in [0,1] decrease when more factors are included.

   theorem prod_antitone_of_unitInterval {S T : Finset I} {f : I → ℝ}
       (hST : S ⊆ T) (h0 : ∀ i ∈ T, 0 ≤ f i) (h1 : ∀ i ∈ T, f i ≤ 1) :
       (∏ i ∈ T, f i) ≤ ∏ i ∈ S, f i := by
   …

8. theorem OAI.QuantitativeVanDerWaerden.FiniteLocalLemma.avoid_union_lower line 66

   Source documentation

   Iterating bounds on intersections with one bad event yields the lower bound for avoiding a finite collection of further events.

   theorem avoid_union_lower (P : Probability Ω) (bad : I → Finset Ω)
       (z : I → ℝ) (target S U : Finset I)
       (hz : ∀ i, 0 ≤ 1 - z i)
       (hST : S ⊆ target) (hUT : U ⊆ target) (hSU : Disjoint S U)
       (hcond : ∀ R, R ⊂ target → ∀ i, i ∉ R →
         P.mass (bad i ∩ avoid bad R) ≤ z i * P.mass (avoid bad R)) :
       P.mass (avoid bad S) * (∏ i ∈ U, (1 - z i)) ≤
         P.mass (avoid bad (S ∪ U)) := by
   …

   Mentions: OAI.QuantitativeVanDerWaerden.FiniteLocalLemma.Probability, OAI.QuantitativeVanDerWaerden.FiniteLocalLemma.avoid

9. theorem OAI.QuantitativeVanDerWaerden.FiniteLocalLemma.positive_and_conditional_bound line 107

   Source documentation

   The simultaneous induction behind the asymmetric local lemma.

   theorem positive_and_conditional_bound (P : Probability Ω) (bad : I → Finset Ω)
       (neighbors : I → Finset I) (z : I → ℝ)
       (hzpos : ∀ i, 0 < z i) (hzlt : ∀ i, z i < 1)
       (hindependent : ∀ i T, i ∉ T → Disjoint T (neighbors i) →
         P.mass (bad i ∩ avoid bad T) = P.mass (bad i) * P.mass (avoid bad T))
       (hcriterion : ∀ i, P.mass (bad i) ≤ z i * ∏ j ∈ neighbors i, (1 - z j))
       (T : Finset I) :
       0 < P.mass (avoid bad T) ∧
         ∀ i, i ∉ T → P.mass (bad i ∩ avoid bad T) ≤ z i * P.mass (avoid bad T) := by
   …

   Mentions: OAI.QuantitativeVanDerWaerden.FiniteLocalLemma.Probability, OAI.QuantitativeVanDerWaerden.FiniteLocalLemma.avoid

10. theorem OAI.QuantitativeVanDerWaerden.FiniteLocalLemma.finite_asymmetric_local_lemma line 168

    Source documentation

    Finite asymmetric local lemma, stated for a finite additive probability.

    theorem finite_asymmetric_local_lemma [Fintype I]
        (P : Probability Ω) (bad : I → Finset Ω) (neighbors : I → Finset I)
        (z : I → ℝ) (hzpos : ∀ i, 0 < z i) (hzlt : ∀ i, z i < 1)
        (hindependent : ∀ i T, i ∉ T → Disjoint T (neighbors i) →
          P.mass (bad i ∩ avoid bad T) = P.mass (bad i) * P.mass (avoid bad T))
        (hcriterion : ∀ i, P.mass (bad i) ≤ z i * ∏ j ∈ neighbors i, (1 - z j)) :
        0 < P.mass (avoid bad Finset.univ) :=
    …

    Mentions: OAI.QuantitativeVanDerWaerden.FiniteLocalLemma.Probability, OAI.QuantitativeVanDerWaerden.FiniteLocalLemma.avoid

11. theorem OAI.QuantitativeVanDerWaerden.FiniteLocalLemma.exists_avoiding line 178
12. theorem OAI.QuantitativeVanDerWaerden.FiniteLocalLemma.finite_asymmetric_local_lemma_weights line 195