OAI/NumberTheory/Ostmann/Construction/OriginalSeparatedBulkBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.original_separated_bulk_bound line 15

   Source documentation

   Compose Page replacement, the separated signed estimate, restoration of omitted primes and collision removal without changing the original normalizers.

   theorem original_separated_bulk_bound {I J C : Type*}
       [Fintype I] [Fintype J] [Fintype C]
       (r : ℕ) [NeZero r] (p : I → ℕ) [∀ i, NeZero (p i)]
       [NeZero (∏ i, bulkResidueModuli r p i)]
       (hc : Pairwise (fun i j => (bulkResidueModuli r p i).Coprime (bulkResidueModuli r p j)))
       (primes : Finset ℕ) (u v : J → C → ℝ) (hu : ∀ j c, 0 < u j c)
       (c₀ : C × (ZMod (∏ i, bulkResidueModuli r p i))ˣ)
       (hP : ∀ j, primeCellSupport (∏ i, bulkResidueModuli r p i)
         (fun c : C × (ZMod (∏ i, bulkResidueModuli r p i))ˣ => c.2.val.val)
         (fun c => u j c.1) (fun c => v j c.1) ⊆ primes)
       (hsep : ∀ j (c d : C × (ZMod (∏ i, bulkResidueModuli r p i))ˣ), c ≠ d →
         ¬Nat.ModEq (∏ i, bulkResidueModuli r p i) c.2.val.val d.2.val.val ∨
   …

   Mentions: OAI.Ostmann.bulkResidueModuli, OAI.Ostmann.primes, OAI.Ostmann.primeCellSupport

2. theorem OAI.Ostmann.original_bulk_main_gain line 76

   Source documentation

   At the actual tree-and-word cardinalities, the separated main term has any prescribed fixed exponential saving after the quartet tolerance is chosen.

   theorem original_bulk_main_gain {n m : ℕ} (C D W A δ E : ℝ)
       (hW : 0 ≤ W) (hA : 0 ≤ A) (hδ : 0 ≤ δ)
       (hAexp : A ≤ Real.exp (C * m)) (hδgain : δ ≤ signedBulkGainTarget n C D)
       (z : ℂ)
       (hz : ‖z‖ ≤ (W * A) * 4 ^ Fintype.card (TreeLeafIndex n × Fin m) *
         δ ^ Fintype.card (Fin m) + E) :
       ‖z‖ ≤ W * Real.exp (-D * m) + E := by
   …

   Mentions: OAI.Ostmann.signedBulkGainTarget, OAI.Ostmann.TreeLeafIndex