OAI/NumberTheory/Ostmann/Arithmetic/MovingInternalProbabilityError.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingInternalBaseFactor_norm_average line 12

   Source documentation

   The base coefficient is a nonnegative indicator, so its absolute average is exactly its simultaneous line probability.

   theorem movingInternalBaseFactor_norm_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

2. theorem OAI.Ostmann.movingInternalPairFactor_probability_error line 30
3. theorem OAI.Ostmann.movingInternalPairFactor_probability_norm_le line 48