OAI/NumberTheory/Ostmann/Arithmetic/BulkResidueCRT.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.bulkResidueModuli line 12

   Source documentation

   The only moduli remaining after the internal line comparison.

   def bulkResidueModuli {I : Type*} (r : ℕ) (p : I → ℕ) : Unit ⊕ I → ℕ
     | .inl _ => r
     | .inr i => p i

2. def OAI.Ostmann.bulkResidueAssemble line 16
3. def OAI.Ostmann.bulkResidueEquiv line 24

   Source documentation

   Simultaneous CRT on all bulk slots, transposed into one frequency block and one block for each spectator.

   noncomputable def bulkResidueEquiv {I J : Type*} [Fintype I]
       (r : ℕ) (p : I → ℕ)
       (hc : Pairwise (fun i j => (bulkResidueModuli r p i).Coprime (bulkResidueModuli r p j))) :
       (J → (ZMod (∏ i, bulkResidueModuli r p i))ˣ) ≃
         (J → (ZMod r)ˣ) × (∀ i, J → (ZMod (p i))ˣ) where
   …

   Mentions: OAI.Ostmann.bulkResidueModuli

4. theorem OAI.Ostmann.bulkResidueEquiv_frequency_modEq line 48
5. theorem OAI.Ostmann.bulkResidueEquiv_page line 69

   Source documentation

   The conductor deletion confines every retained Page factor to the frequency residue array.

   theorem bulkResidueEquiv_page {I J : Type*} [Fintype I]
       (r : ℕ) [NeZero r] (p : I → ℕ)
       [NeZero (∏ i, bulkResidueModuli r p i)]
       (hc : Pairwise (fun i j => (bulkResidueModuli r p i).Coprime (bulkResidueModuli r p j)))
       (P : PublishedProgressionInput) (Q : ℕ)
       (hpage : pageAtModulus (∏ i, bulkResidueModuli r p i) (selectedPageZero P Q) =
         pageAtModulus r (selectedPageZero P Q))
       (x : J → (ZMod (∏ i, bulkResidueModuli r p i))ˣ) (j : J) (y : ℝ) :
       pageGiantWeight P Q (∏ i, bulkResidueModuli r p i) (x j).val.val y =
         pageGiantWeight P Q r ((bulkResidueEquiv r p hc x).1 j).val.val y := by
   …

   Mentions: OAI.Ostmann.bulkResidueModuli, OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.pageAtModulus, OAI.Ostmann.selectedPageZero, OAI.Ostmann.pageGiantWeight, OAI.Ostmann.bulkResidueEquiv

6. theorem OAI.Ostmann.bulk_residue_page_average line 85

   Source documentation

   Exact joint factorization, for arbitrary complex frequency amplitudes. The spectator main terms have no residue-count or partition-count loss.

   theorem bulk_residue_page_average {I J : Type*} [Fintype I] [Fintype J]
       (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)))
       (P : PublishedProgressionInput) (Q : ℕ)
       (hpage : pageAtModulus (∏ i, bulkResidueModuli r p i) (selectedPageZero P Q) =
         pageAtModulus r (selectedPageZero P Q))
       (y : J → ℝ) (F : (J → (ZMod r)ˣ) → ℂ) (G : ∀ i, (J → (ZMod (p i))ˣ) → ℂ) :
       (Fintype.card (J → (ZMod (∏ i, bulkResidueModuli r p i))ˣ) : ℂ)⁻¹ *
         (∑ x, (F (bulkResidueEquiv r p hc x).1 *
           ∏ j, pageGiantWeight P Q (∏ i, bulkResidueModuli r p i) (x j).val.val (y j)) *
           ∏ i, G i ((bulkResidueEquiv r p hc x).2 i)) =
   …

   Mentions: OAI.Ostmann.bulkResidueModuli, OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.pageAtModulus, OAI.Ostmann.selectedPageZero, OAI.Ostmann.bulkResidueEquiv, OAI.Ostmann.pageGiantWeight