OAI/NumberTheory/Ostmann/Arithmetic/MovingInternalBaseAverage.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingInternalBaseFactor line 11
2. theorem OAI.Ostmann.movingInternalBaseFactor_average line 21

   Source documentation

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

   theorem movingInternalBaseFactor_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 true
         (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

3. theorem OAI.Ostmann.movingInternalBaseProbability_eq_flags line 48

   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 movingInternalBaseProbability_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 true
         (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