OAI/NumberTheory/TwoPoint/Walks/WitnessSegmentation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Explicit finite metadata for splitting one recorded word into witness paths.

  1. abbrev OAI.TwoPointCorrelations.WitnessSegmentation line 11
  2. lemma OAI.TwoPointCorrelations.card_witnessSegmentation line 14
  3. lemma OAI.TwoPointCorrelations.witnessSegmentation_cost line 20
  4. lemma OAI.TwoPointCorrelations.sum_le_of_card_mul_le line 49

    Source documentation

    A common scalar bound with the exact finite cardinality pays for every record.

    lemma sum_le_of_card_mul_le {ι : Type*} [Fintype ι] [Nonempty ι]
    (f : ι → ℝ) (B : ℝ) (hf : ∀ i, (Fintype.card ι : ℝ) * f i ≤ B) :
    ∑ i, f i ≤ B := by
…