OAI/NumberTheory/Ostmann/Arithmetic/MovingPrimeBaseAverage.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingInternalBaseFactor_prime_average line 13

   Source documentation

   The field average is the exact simultaneous line probability for all occurrences of the prime in both original histories.

   theorem movingInternalBaseFactor_prime_average {σ : Type*} {n : ℕ}
       (value : σ → ℕ) (T : Bool → MovingSlotData σ n) (p : ℕ) [Fact p.Prime] :
       (Fintype.card ((ZMod p)ˣ × (ZMod p)ˣ) : ℂ)⁻¹ *
         (∑ z : (ZMod p)ˣ × (ZMod p)ˣ, movingInternalBaseFactor value T p z.1 z.2) =
       (internalLineProbability false
         (fun j => MovingSlotReversal.naturalReduction p value
           (movingPrimeOccurrenceLine value T p j).a)
         (fun j => MovingSlotReversal.naturalReduction p value
           (movingPrimeOccurrenceLine value T p j).b) : ℂ) := by
   …

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

2. theorem OAI.Ostmann.movingInternalPrimeProbability_eq_flags line 40

   Source documentation

   All rows and all cleared denominators in this line probability come from the actual moving trees. Thus the polynomial flags used later are exact.

   theorem movingInternalPrimeProbability_eq_flags {σ : Type*} {n : ℕ}
       (tier : σ → ℕ) (value : σ → ℕ) (hprime : ∀ i, (value i).Prime)
       (hdisjoint : ∀ i j, tier i ≠ tier j → value i ≠ value j)
       (T : Bool → MovingSlotData σ n) (hlevels : ∀ side, (T side).Levels tier)
       (p : ℕ) [Fact p.Prime]
       (hf : ∀ side, (T side).Frequencies (fun s => (s : ZMod p) ≠ 0))
       (base : MovingPrimeOccurrences value T p) :
       internalLineProbability false
         (fun j => MovingSlotReversal.naturalReduction p value
           (movingPrimeOccurrenceLine value T p j).a)
         (fun j => MovingSlotReversal.naturalReduction p value
           (movingPrimeOccurrenceLine value T p j).b) =
   …

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