BlockCoverage.lean`

23 declarations, 0 contain sorry, 0 declared as axioms

Coverage by full blocks containing a heavy position

The bth full block consists literally of positions b * h + z, for z < h. Every full block that is not used consists of light positions. Counting the disjoint full blocks and the final remainder transfers bounds within used blocks to counts in the entire interval.

def OAI.QuantitativeVanDerWaerden.BlockCoverage.blockIndex line 25
Source documentation
Position z in full block b.
```
def blockIndex (k h : ℕ) (b : Fin (k / h)) (z : Fin h) : Fin k :=
…
```
theorem OAI.QuantitativeVanDerWaerden.BlockCoverage.blockIndex_val line 34
theorem OAI.QuantitativeVanDerWaerden.BlockCoverage.blockIndex_div line 37
theorem OAI.QuantitativeVanDerWaerden.BlockCoverage.blockIndex_injective line 44
def OAI.QuantitativeVanDerWaerden.BlockCoverage.blockPositions line 51
theorem OAI.QuantitativeVanDerWaerden.BlockCoverage.card_blockPositions line 55
theorem OAI.QuantitativeVanDerWaerden.BlockCoverage.blockPositions_disjoint line 60
def OAI.QuantitativeVanDerWaerden.BlockCoverage.blockUnion line 72
theorem OAI.QuantitativeVanDerWaerden.BlockCoverage.blockUnion_mono line 75
theorem OAI.QuantitativeVanDerWaerden.BlockCoverage.card_blockUnion line 81
def OAI.QuantitativeVanDerWaerden.BlockCoverage.usedBlocks line 87
theorem OAI.QuantitativeVanDerWaerden.BlockCoverage.mem_usedBlocks line 92
def OAI.QuantitativeVanDerWaerden.BlockCoverage.lightPositions line 97
def OAI.QuantitativeVanDerWaerden.BlockCoverage.lightCount line 101
theorem OAI.QuantitativeVanDerWaerden.BlockCoverage.unused_full_positions_light line 105
Source documentation
Every full-block position not covered by a used block is light.
```
theorem unused_full_positions_light (k h : ℕ) (heavy : Fin k → Prop)
    [DecidablePred heavy] :
    blockUnion k h Finset.univ \ blockUnion k h (usedBlocks k h heavy) ⊆
      lightPositions heavy := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.BlockCoverage.blockUnion, OAI.QuantitativeVanDerWaerden.BlockCoverage.usedBlocks, OAI.QuantitativeVanDerWaerden.BlockCoverage.lightPositions
theorem OAI.QuantitativeVanDerWaerden.BlockCoverage.full_positions_le_light_add_used line 122
theorem OAI.QuantitativeVanDerWaerden.BlockCoverage.usedBlocks_mul_lower line 136
Source documentation
The final remainder has fewer than h positions, and unused full blocks are charged to individual light positions.
```
theorem usedBlocks_mul_lower (k h : ℕ) (hh : 0 < h)
    (heavy : Fin k → Prop) [DecidablePred heavy] :
    (k : ℝ) - (h : ℝ) - (lightCount heavy : ℝ) ≤
      ((usedBlocks k h heavy).card : ℝ) * (h : ℝ) := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.BlockCoverage.lightCount, OAI.QuantitativeVanDerWaerden.BlockCoverage.usedBlocks
theorem OAI.QuantitativeVanDerWaerden.BlockCoverage.usedPositions_lower line 148
def OAI.QuantitativeVanDerWaerden.BlockCoverage.blockColorCount line 155
def OAI.QuantitativeVanDerWaerden.BlockCoverage.colorCount line 159
theorem OAI.QuantitativeVanDerWaerden.BlockCoverage.sum_blockColorCount_le line 164
Source documentation
Counts in any collection of distinct full blocks sum to at most the corresponding count in the whole interval.
```
theorem sum_blockColorCount_le (k h : ℕ) (hh : 0 < h)
    (B : Finset (Fin (k / h))) (color : Fin k → Bool) (c : Bool) :
    (∑ b ∈ B, blockColorCount k h color c b) ≤ colorCount color c := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.BlockCoverage.blockColorCount, OAI.QuantitativeVanDerWaerden.BlockCoverage.colorCount
theorem OAI.QuantitativeVanDerWaerden.BlockCoverage.colorCount_lower line 182
Source documentation
If every used full block contains at least h/8 positions of a specified color, that color occupies at least (k-h-lightCount)/8 positions globally.
```
theorem colorCount_lower (k h : ℕ) (hh : 0 < h)
    (heavy : Fin k → Prop) [DecidablePred heavy]
    (color : Fin k → Bool) (c : Bool)
    (hblocks : ∀ b ∈ usedBlocks k h heavy,
      (h : ℝ) / 8 ≤ (blockColorCount k h color c b : ℝ)) :
    ((k : ℝ) - (h : ℝ) - (lightCount heavy : ℝ)) / 8 ≤
      (colorCount color c : ℝ) := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.BlockCoverage.usedBlocks, OAI.QuantitativeVanDerWaerden.BlockCoverage.blockColorCount, OAI.QuantitativeVanDerWaerden.BlockCoverage.lightCount, OAI.QuantitativeVanDerWaerden.BlockCoverage.colorCount
theorem OAI.QuantitativeVanDerWaerden.BlockCoverage.colorCount_tenth line 202
Source documentation
The one-tenth light-position and block-size bounds give the desired one-tenth global count for each color.
```
theorem colorCount_tenth (k h : ℕ) (hh : 0 < h)
    (heavy : Fin k → Prop) [DecidablePred heavy]
    (color : Fin k → Bool)
    (hlight : (lightCount heavy : ℝ) ≤ (k : ℝ) / 10)
    (hsmall : (h : ℝ) ≤ (k : ℝ) / 10)
    (hblocks : ∀ b ∈ usedBlocks k h heavy, ∀ c : Bool,
      (h : ℝ) / 8 ≤ (blockColorCount k h color c b : ℝ)) :
    ∀ c : Bool, (k : ℝ) / 10 ≤ (colorCount color c : ℝ) := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.BlockCoverage.lightCount, OAI.QuantitativeVanDerWaerden.BlockCoverage.usedBlocks, OAI.QuantitativeVanDerWaerden.BlockCoverage.blockColorCount, OAI.QuantitativeVanDerWaerden.BlockCoverage.colorCount