OAI/Combinatorics/ProgressionColoring/OuterIncidence.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.QuantitativeVanDerWaerden.outer_weight_le_of_support_lower line 11
2. theorem OAI.QuantitativeVanDerWaerden.outer_weight_le_of_half_length line 16
3. theorem OAI.QuantitativeVanDerWaerden.outer_total_weight_bound line 22
4. theorem OAI.QuantitativeVanDerWaerden.outer_local_incident_bound line 35

   Source documentation

   The anchored count through one label gives the local incident-weight bound, after grouping actual pattern indices by their return period.

   theorem outer_local_incident_bound {I : Type uI} {Label : Type uLabel} [Fintype I] [DecidableEq I]
       [DecidableEq Label] (support : I → Finset Label) (period : I → ℕ)
       (periods : Finset ℕ) (countBound : ℕ → ℕ)
       (hperiod : ∀ i, period i ∈ periods)
       (hsize : ∀ i, period i ≤ 2 * (support i).card)
       (hcount : ∀ b h,
         (Finset.univ.filter (fun i => b ∈ support i ∧ period i = h)).card ≤ countBound h)
       (b : Label) :
       ∑ i ∈ Finset.univ.filter (fun i => b ∈ support i),
           Real.exp (-((support i).card : ℝ) / 32) ≤
         ∑ h ∈ periods, (countBound h : ℝ) * Real.exp (-(h : ℝ) / 64) := by
   …