OAI/NumberTheory/Ostmann/Construction/InitialSpectatorFourier.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingRegularTransform_sum line 11

   Source documentation

   A sum-indexed transform splits without any coprimality assumption.

   theorem movingRegularTransform_sum {I J : Type*} [Fintype I] [Fintype J]
       (p : I ⊕ J → ℕ) [∀ i, NeZero (p i)] (g : ∀ i, ZMod (p i) → ℂ)
       (D : ℕ) (s : ℤ) :
       movingRegularTransform p g D s =
         movingRegularTransform (fun i => p (.inl i)) (fun i => g (.inl i))
           (D * ∏ j, p (.inr j)) s *
         movingRegularTransform (fun j => p (.inr j)) (fun j => g (.inr j))
           (D * ∏ i, p (.inl i)) s := by
   …

   Mentions: OAI.Ostmann.movingRegularTransform

2. theorem OAI.Ostmann.primeTupleFourierCoefficient_split line 40

   Source documentation

   Reindexing a full original tuple separates exactly the fixed spectators from the retained primes, including both original CRT cofactors.

   theorem primeTupleFourierCoefficient_split {I J : Type*} [Fintype I] [Fintype J]
       {n : ℕ} (e : I ⊕ J ≃ Fin n) (P : Finset ℕ) [∀ p : P, NeZero (p : ℕ)]
       (F : Fin n → (p : P) → ZMod (p : ℕ) → ℂ)
       (ψ : 𝓢(ℝ, ℂ)) (X : ℝ) (V : ℕ) (x : Fin n → P) :
       primeTupleFourierCoefficient P F ψ X V x =
         ∑ v ∈ transferFrequencyRange V,
           normalizedFourierProfile (fun t => 𝓕 ψ t) v ((∏ i, (x i : ℕ)) / X) *
             (movingRegularTransform (fun i => (x (e (.inl i)) : ℕ))
               (fun i => densityFourier (F (e (.inl i)) (x (e (.inl i)))))
               (∏ j, (x (e (.inr j)) : ℕ)) v *
             movingRegularTransform (fun j => (x (e (.inr j)) : ℕ))
               (fun j => densityFourier (F (e (.inr j)) (x (e (.inr j)))))
   …

   Mentions: OAI.Ostmann.primeTupleFourierCoefficient, OAI.Ostmann.transferFrequencyRange, OAI.Ostmann.normalizedFourierProfile, OAI.Ostmann.movingRegularTransform, OAI.Ostmann.densityFourier

3. theorem OAI.Ostmann.movingTaggedTransform_spectator_split line 61

   Source documentation

   A regular spectator block factors from the tagged giant/regular block.

   theorem movingTaggedTransform_spectator_split {I J : Type*} [Fintype I] [Fintype J]
       (q : I → ℕ) (p : J → ℕ) (hq : ∀ i, q i ≠ 0) (hp : ∀ j, p j ≠ 0)
       (tag : J → Bool) (g h : ∀ q : ℕ, ZMod q → ℂ) (fav : ℕ → Bool) (D : ℕ) (s : ℤ) :
       movingTaggedTransform (Sum.elim q p) (Sum.elim (fun _ => false) tag) g h fav D s =
         (∏ i, g (q i) ((s : ZMod (q i)) * ((D * (∏ j, p j) * tupleCofactor q i : ℕ) : ZMod (q i))⁻¹)) *
           movingTaggedTransform p tag g h fav (D * ∏ i, q i) s := by
   …

   Mentions: OAI.Ostmann.movingTaggedTransform, OAI.Ostmann.tupleCofactor

4. def OAI.Ostmann.initialSpectatorCofactor line 86

   Source documentation

   The fixed spectator units are their true cofactors in the spectator list.

   noncomputable def initialSpectatorCofactor {I : Type*} [Fintype I]
       (q : I → ℕ) (hc : Pairwise (fun i j => (q i).Coprime (q j))) (i : I) :
       (ZMod (q i))ˣ :=
   …

5. theorem OAI.Ostmann.initialSpectatorCofactor_val line 91
6. theorem OAI.Ostmann.initial_spectator_transform line 97

   Source documentation

   This is precisely the spectator leaf used throughout the moving recursion.

   theorem initial_spectator_transform {I : Type*} [Fintype I]
       (q : I → ℕ) [∀ i, Fact (q i).Prime]
       (hc : Pairwise (fun i j => (q i).Coprime (q j)))
       (g : ∀ i, ZMod (q i) → ℂ) (M : ℕ) (s : ℤ) :
       movingRegularTransform q g M s =
         ∏ i, spectatorHistoryLeaf (fun _ : Unit => M) (g i)
           (initialSpectatorCofactor q hc i) () s := by
   …

   Mentions: OAI.Ostmann.movingRegularTransform, OAI.Ostmann.spectatorHistoryLeaf, OAI.Ostmann.initialSpectatorCofactor