OAI/NumberTheory/Ostmann/Arithmetic/BulkWeightedErrorBudget.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.bulkPrimeErrorFactor_nonneg line 11
2. theorem OAI.Ostmann.bulkPrimeErrorFactor_antitone line 17
3. theorem OAI.Ostmann.bulkKernelPairComparisonBudget_nonneg line 37
4. theorem OAI.Ostmann.bulk_weighted_error_budget line 44

   Source documentation

   Every residue and real cell in the actual comparison is counted here; only the smallest lower endpoint is used for the progression saving.

   theorem bulk_weighted_error_budget {J Cell : Type*} [Fintype J] [Fintype Cell]
       (P : PublishedProgressionInput) {Q M : ℕ} [NeZero M] (hQ : 2 ≤ Q)
       (Z : J → ℝ) (hZ : ∀ j, 0 ≤ Z j)
       (a : (J → (ZMod M)ˣ) → ℂ) (A : ℝ) (hA : 0 ≤ A) (ha : ∀ z, ‖a z‖ ≤ A)
       (u : J → Cell → ℝ) (T : ℝ) (hu : ∀ j c, T ≤ u j c)
       (B : ℝ) (hB : 0 ≤ B) :
       (∏ j, Z j) * ∑ c : J → Cell, ∑ z : J → (ZMod M)ˣ, ‖a z‖ *
         (2 ^ Fintype.card J * ∑ j, B * bulkPrimeErrorFactor P Q (u j (c j))) ≤
       ((∏ j, Z j) * (Fintype.card Cell : ℝ) ^ Fintype.card J *
         (Fintype.card (ZMod M)ˣ : ℝ) ^ Fintype.card J * A *
         2 ^ Fintype.card J * (Fintype.card J : ℝ) * B) * bulkPrimeErrorFactor P Q T := by
   …

   Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.bulkPrimeErrorFactor