OAI/NumberTheory/TwoPoint/Bounds/PrimeSlotClasses.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TwoPointCorrelations.CrudeWordCode.recordedSlots line 18
2. def OAI.TwoPointCorrelations.CrudeWordCode.KindConsistent line 21
3. def OAI.TwoPointCorrelations.CrudeWordCode.RowInjective line 24
4. def OAI.TwoPointCorrelations.CrudeWordCode.tupleClasses line 27
5. def OAI.TwoPointCorrelations.CrudeWordCode.tupleLabels line 30
6. lemma OAI.TwoPointCorrelations.CrudeWordCode.classAt_mem_tupleClasses line 33
7. lemma OAI.TwoPointCorrelations.CrudeWordCode.classAt_notMem_tupleClasses line 38
8. lemma OAI.TwoPointCorrelations.CrudeWordCode.tuple_product line 45

   Source documentation

   Rowwise squarefreeness makes the tuple product a product over its classes.

   lemma tuple_product (c : CrudeWordCode R N R) (hc : c.KindConsistent)
       (hi : c.RowInjective) (i : Fin R) (a : c.tupleClasses → ℕ)
       (b : {z : c.usedClasses // z ∉ c.tupleClasses} → ℕ) :
       (∏ j ∈ c.recordedSlots i false,
         joinCoordinates c.tupleClasses a b (c.classAt j)) =
           ∏ z ∈ c.tupleLabels i, a z := by
   …

   Mentions: OAI.TwoPointCorrelations.CrudeWordCode, OAI.TwoPointCorrelations.joinCoordinates

9. lemma OAI.TwoPointCorrelations.CrudeWordCode.padding_product line 64
10. def OAI.TwoPointCorrelations.CrudeWordCode.labeledWord line 75

    Source documentation

    A fixed padding assignment and a tuple-class support define the symbolic word.

    def labeledWord (c : CrudeWordCode R N R)
        (b : {z : c.usedClasses // z ∉ c.tupleClasses} → ℕ) : LabeledPrimeWord c.tupleClasses where
    …

    Mentions: OAI.TwoPointCorrelations.CrudeWordCode, OAI.TwoPointCorrelations.LabeledPrimeWord

11. lemma OAI.TwoPointCorrelations.CrudeWordCode.labeledWord_length line 81
12. theorem OAI.TwoPointCorrelations.CrudeWordCode.labeledWord_resample line 86

    Source documentation

    Resampling changes exactly the tuple primes, with no additional padding choices.

    theorem labeledWord_resample (c : CrudeWordCode R N R) (hc : c.KindConsistent)
        (hi : c.RowInjective) (a : c.tupleClasses → ℕ)
        (b : {z : c.usedClasses // z ∉ c.tupleClasses} → ℕ) :
        ((c.labeledWord b).resample a).word =
          c.numericalWord (joinCoordinates c.tupleClasses a b) := by
    …

    Mentions: OAI.TwoPointCorrelations.CrudeWordCode, OAI.TwoPointCorrelations.joinCoordinates