OAI/NumberTheory/TwoPoint/Bounds/EncodedWitnessSum.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Sum the numerical singleton-witness event over the complete prime-slot catalog.

  1. def OAI.TwoPointCorrelations.PrimeWordEncoding.Witnesses line 14

    Source documentation

    The main path and all attached witnesses are segments of one recorded word.

    def PrimeWordEncoding.Witnesses {R T : ℕ} {P Q : Finset ℕ}
    (e : PrimeWordEncoding R T P Q) (n mainLength : ℕ) (start len : Fin n → ℕ)
    (h s J : ℕ) (supply : ℕ → ℕ → Prop) : Prop :=
…

    Mentions: OAI.TwoPointCorrelations.PrimeWordEncoding

  2. theorem OAI.TwoPointCorrelations.encoded_witness_sum_le line 22