OAI/NumberTheory/Ostmann/Arithmetic/MovingTemplateSupport.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingTemplateSlotList line 17
2. theorem OAI.Ostmann.mem_movingTemplateSlotList line 21
3. theorem OAI.Ostmann.prime_pairwise_list_nodup line 29
4. theorem OAI.Ostmann.movingTemplateCoefficient_nonzero_injective line 42

   Source documentation

   The support of the actual coefficient forces every prime in the full regular template to be distinct.

   theorem movingTemplateCoefficient_nonzero_injective {σ : Type} [Fintype σ]
       (value : σ → ℕ) (outside : List ℕ) (μ : ℕ → σ → ℝ)
       (childBound pivotBound V : ℕ → ℕ) (F : MovingSlotState σ → ℤ → ℂ)
       (φ : ℝ → ℝ) (G : ℕ → ℝ) (n r m : ℕ) (s : ℤ)
       (y : MovingRegularSlot n r m → σ) (XL XR : ℕ)
       (hprime : ∀ i, (value (y i)).Prime)
       (h : movingTemplateCoefficient value outside μ childBound pivotBound V F φ G n r m s y XL XR ≠ 0) :
       Function.Injective (value ∘ y) := by
   …

   Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.MovingRegularSlot, OAI.Ostmann.movingTemplateCoefficient

5. theorem OAI.Ostmann.movingTemplateCoefficient_full_transform line 66

   Source documentation

   The two phase factors and the regular product transform combine into exactly the full indexed Fourier transform wherever the coefficient contributes.

   theorem movingTemplateCoefficient_full_transform {σ : Type} [Fintype σ]
       (value : σ → ℕ) (outside : List ℕ) (μ : ℕ → σ → ℝ)
       (childBound pivotBound V : ℕ → ℕ) (F : MovingSlotState σ → ℤ → ℂ)
       (φ : ℝ → ℝ) (G : ℕ → ℝ) (n r m : ℕ) (s : ℤ)
       (y : MovingRegularSlot n r m → σ) (q : Bool → ℕ) [∀ b, Fact (q b).Prime]
       (hprime : ∀ i, (value (y i)).Prime)
       (greg ggiant : ∀ p : ℕ, ZMod p → ℂ) (favorable : ℕ → Bool) :
       let _ : ∀ i, Fact ((value ∘ y) i).Prime := fun i => ⟨hprime i⟩
   …

   Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.MovingRegularSlot