OAI/NumberTheory/Ostmann/Arithmetic/MovingRepresentativeLineSystem.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Ostmann.MovingPairRepresentativeOccurrences line 10
2. def OAI.Ostmann.movingRepresentativeLine line 14
3. theorem OAI.Ostmann.movingPrimeLineSystem_representative_iff line 22

   Source documentation

   On samples with distinct prime values, all occurrences of the selected prime are precisely the fixed occurrences of its representative slot.

   theorem movingPrimeLineSystem_representative_iff {σ : Type*} {n : ℕ}
       (value : σ → ℕ) (T : Bool → MovingSlotData σ n) (rep : σ)
       (hunique : ∀ i, value i = value rep → i = rep)
       (x y : ZMod (value rep)) :
       (∀ j : MovingPrimeOccurrences value T (value rep),
         let φ := MovingSlotReversal.naturalReduction (value rep) value
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.MovingPrimeOccurrences, OAI.Ostmann.MovingSlotReversal.naturalReduction

4. theorem OAI.Ostmann.movingInternalBaseProbability_representative line 48

   Source documentation

   This reindexing fixes the polynomial family before the prime values are sampled, as required by the joint small-prime coincidence theorem.

   theorem movingInternalBaseProbability_representative {σ : Type*} {n : ℕ}
       (value : σ → ℕ) (T : Bool → MovingSlotData σ n) (rep : σ)
       [Fact (value rep).Prime] (hunique : ∀ i, value i = value rep → i = rep) :
       internalLineProbability true
         (fun j => MovingSlotReversal.naturalReduction (value rep) value
           (movingPrimeOccurrenceLine value T (value rep) j).a)
         (fun j => MovingSlotReversal.naturalReduction (value rep) value
           (movingPrimeOccurrenceLine value T (value rep) j).b) =
       internalLineProbability true
         (fun j => MovingSlotReversal.naturalReduction (value rep) value
           (movingRepresentativeLine T rep j).a)
         (fun j => MovingSlotReversal.naturalReduction (value rep) value
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.internalLineProbability, OAI.Ostmann.MovingSlotReversal.naturalReduction, OAI.Ostmann.movingPrimeOccurrenceLine, OAI.Ostmann.movingRepresentativeLine