OAI/NumberTheory/Ostmann/Arithmetic/MovingFullTransformTransfer.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.moving_full_transform_guarded line 20

   Source documentation

   The row used by Cauchy is the actual extracted part of the full transform. The support conditions are used only where the original coefficient is nonzero.

   theorem moving_full_transform_guarded {J H : Type*} [Fintype J] [Fintype H]
       (Q : J → ℕ) (L : H → ℕ) [∀ j, Fact (Q j).Prime] [∀ i, Fact (L i).Prime]
       (gQ : ∀ j, ZMod (Q j) → ℂ) (gL : ∀ i, ZMod (L i) → ℂ)
       (D M : ℕ) (hM : (∏ j, Q j) = M) (hMpos : 0 < M) (v : ℤ)
       (hQ : Pairwise (fun i j => (Q i).Coprime (Q j)))
       (hD : ∀ j, D.Coprime (Q j)) (hL : (∏ i, L i).Coprime M) :
       movingRegularTransform (Sum.elim Q L)
           (movingSumFactors Q L gQ gL) D v =
         movingGuardedRow Q gQ D (positiveIntegerPivotKey M hMpos (∏ i, L i) v) *
           movingRegularTransform L gL (M * D) v := by
   …

   Mentions: OAI.Ostmann.movingRegularTransform, OAI.Ostmann.movingSumFactors, OAI.Ostmann.movingGuardedRow, OAI.Ostmann.positiveIntegerPivotKey

2. theorem OAI.Ostmann.smoothGiantPrior_full_transform_transfer line 44

   Source documentation

   One iteration for the genuine full Fourier transform. The row energy is derived from the normalized compensation transforms, and the retained factors are evaluated at the exact new frequency after the forced integer substitution.

   theorem smoothGiantPrior_full_transform_transfer
       {Y A J H : Type*} [Fintype Y] [Fintype A] [Fintype J] [Fintype H]
       (P I : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) (hPI : P ⊆ I)
       (hI : ∀ p ∈ I, 0 < p)
       (φ : ℝ → ℝ) (G : ℝ) (hφ : ∀ x, 0 ≤ φ x)
       (hpos : 0 < smoothGiantMass P φ G)
       (μ : Y → ℝ) (hμ : ∀ y, 0 ≤ μ y) (hμmass : ∑ y, μ y = 1)
       (U : Y → ℕ) (hU : ∀ y, 0 < U y)
       (Q : Y → P → J → ℕ) [∀ y p j, Fact (Q y p j).Prime]
       (gQ : ∀ y p j, ZMod (Q y p j) → ℂ)
       (hQprod : ∀ y p, (∏ j, Q y p j) = (p : ℕ) * U y)
       (giant : J) (S : ∀ y p j, Finset (ZMod (Q y p j)))
   …

   Mentions: OAI.Ostmann.smoothGiantMass