OAI/NumberTheory/Ostmann/Arithmetic/MovingInternalProductError.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingInternalHaarAverage line 11
2. def OAI.Ostmann.movingInternalLineProbability line 16
3. theorem OAI.Ostmann.movingInternalLineProbability_nonneg line 24
4. theorem OAI.Ostmann.movingInternalLineProbability_le_inv line 28
5. theorem OAI.Ostmann.movingInternalProduct_error line 46

   Source documentation

   The simultaneous replacement is relative to the complete product of line probabilities, including the factor from every distinct internal prime.

   theorem movingInternalProduct_error {σ : 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 : Finset ℕ) [∀ p : P, Fact p.val.Prime]
       (hf : ∀ p : P, ∀ side, (T side).Frequencies (fun s => (s : ZMod p.val) ≠ 0)) :
       ‖(∏ p : P, movingInternalHaarAverage value T p.val) -
           ∏ p : P, (movingInternalLineProbability value T p.val : ℂ)‖ ≤
         (2 * (2 ^ n - 1 : ℕ) * ∑ p : P, (p.val : ℝ)⁻¹) *
           ∏ p : P, movingInternalLineProbability value T p.val := by
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.movingInternalHaarAverage, OAI.Ostmann.movingInternalLineProbability

6. theorem OAI.Ostmann.movingInternalProduct_weighted_error line 71

   Source documentation

   The external coefficient may grow with the sampled internal primes. Only its product with the actual line probabilities needs to be bounded.

   theorem movingInternalProduct_weighted_error {σ : 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 : Finset ℕ) [∀ p : P, Fact p.val.Prime]
       (hf : ∀ p : P, ∀ side, (T side).Frequencies (fun s => (s : ZMod p.val) ≠ 0))
       (W : ℂ) (B : ℝ)
       (hW : ‖W‖ * (∏ p : P, movingInternalLineProbability value T p.val) ≤ B) :
       ‖W * ((∏ p : P, movingInternalHaarAverage value T p.val) -
           ∏ p : P, (movingInternalLineProbability value T p.val : ℂ))‖ ≤
         B * (2 * (2 ^ n - 1 : ℕ) * ∑ p : P, (p.val : ℝ)⁻¹) := by
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.movingInternalLineProbability, OAI.Ostmann.movingInternalHaarAverage