RegularTuplePoisson.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Initial Poisson summation for the actual normalized residue transforms

theorem OAI.Ostmann.tuple_regular_fourier line 14

Source documentation

Exact normalization and cofactor arguments for arbitrary local tests. This applies to the phase giant and to every normalized residue indicator.

theorem tuple_regular_fourier {I : Type*} [Fintype I]
    (p : I → ℕ) [∀ i, NeZero (p i)] [NeZero (∏ i, p i)]
    (hc : Pairwise (fun i j => (p i).Coprime (p j)))
    (F : ∀ i, ZMod (p i) → ℂ) (v : ℤ) :
    additiveFourier (tupleCRTFunction p hc F) (v : ZMod (∏ i, p i)) =
      (Real.sqrt (∏ i, p i : ℕ) : ℂ)⁻¹ *
        movingRegularTransform p (fun i => densityFourier (F i)) 1 v := by
…

Mentions: OAI.Ostmann.additiveFourier, OAI.Ostmann.tupleCRTFunction, OAI.Ostmann.movingRegularTransform, OAI.Ostmann.densityFourier

theorem OAI.Ostmann.tuple_regular_poisson_normalized line 42

Source documentation

The physical tuple divided by sqrt X is the actual initial regular Fourier amplitude. The sign of the frequency is retained explicitly.

theorem tuple_regular_poisson_normalized {I : Type*} [Fintype I]
    (p : I → ℕ) [∀ i, NeZero (p i)] [NeZero (∏ i, p i)]
    (hc : Pairwise (fun i j => (p i).Coprime (p j)))
    (F : ∀ i, ZMod (p i) → ℂ) (ψ : 𝓢(ℝ, ℂ)) (X : ℝ) (hX : 0 < X) :
    (∑' a : ℤ, (∏ i, F i (a : ZMod (p i))) * ψ ((a : ℝ) / X)) /
        (Real.sqrt X : ℂ) =
      ∑' v : ℤ, (Real.sqrt (X / (∏ i, p i : ℕ)) : ℂ) *
        𝓕 ψ ((v : ℝ) * X / (∏ i, p i : ℕ)) *
          movingRegularTransform p (fun i => densityFourier (F i)) 1 (-v) := by
…

Mentions: OAI.Ostmann.movingRegularTransform, OAI.Ostmann.densityFourier

theorem OAI.Ostmann.tuple_regular_poisson_finite line 71

Source documentation

Compact Fourier support produces a finite integer-frequency amplitude; there is no estimate or discarded tail in this step.

theorem tuple_regular_poisson_finite {I : Type*} [Fintype I]
    (p : I → ℕ) [∀ i, NeZero (p i)] [NeZero (∏ i, p i)]
    (hc : Pairwise (fun i j => (p i).Coprime (p j)))
    (F : ∀ i, ZMod (p i) → ℂ) (ψ : 𝓢(ℝ, ℂ)) (X H : ℝ) (hX : 0 < X) (N : ℕ)
    (hcut : H * (∏ i, p i : ℕ) ≤ N * X)
    (hsupp : ∀ x : ℝ, H < |x| → 𝓕 ψ x = 0) :
    (∑' a : ℤ, (∏ i, F i (a : ZMod (p i))) * ψ ((a : ℝ) / X)) /
        (Real.sqrt X : ℂ) =
      ∑ v ∈ Finset.Icc (-(N : ℤ)) N, (Real.sqrt (X / (∏ i, p i : ℕ)) : ℂ) *
        𝓕 ψ ((v : ℝ) * X / (∏ i, p i : ℕ)) *
          movingRegularTransform p (fun i => densityFourier (F i)) 1 (-v) := by
…

Mentions: OAI.Ostmann.movingRegularTransform, OAI.Ostmann.densityFourier

theorem OAI.Ostmann.tuple_regular_poisson_profile line 102

Source documentation

Reversing the finite frequency interval gives exactly the profile used by the sampled recursion. No symmetry assumption on the Schwartz window is needed: the minus sign belongs to the normalized Fourier profile.

theorem tuple_regular_poisson_profile {I : Type*} [Fintype I]
    (p : I → ℕ) [∀ i, NeZero (p i)] [NeZero (∏ i, p i)]
    (hc : Pairwise (fun i j => (p i).Coprime (p j)))
    (F : ∀ i, ZMod (p i) → ℂ) (ψ : 𝓢(ℝ, ℂ)) (X H : ℝ) (hX : 0 < X) (N : ℕ)
    (hcut : H * (∏ i, p i : ℕ) ≤ N * X)
    (hsupp : ∀ x : ℝ, H < |x| → 𝓕 ψ x = 0) :
    (∑' a : ℤ, (∏ i, F i (a : ZMod (p i))) * ψ ((a : ℝ) / X)) /
        (Real.sqrt X : ℂ) =
      ∑ v ∈ Finset.Icc (-(N : ℤ)) N,
        normalizedFourierProfile (fun t => 𝓕 ψ t) v ((∏ i, p i : ℕ) / X) *
          movingRegularTransform p (fun i => densityFourier (F i)) 1 v := by
…

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

theorem OAI.Ostmann.movingRegularTransform_eq_zero_of_nonunit line 135

Source documentation

A zero-mean local test removes every nonunit frequency at that prime. This supplies the initial frequency guard for both kinds of physical test.

theorem movingRegularTransform_eq_zero_of_nonunit {I : Type*} [Fintype I]
    (p : I → ℕ) [∀ i, Fact (p i).Prime]
    (g : ∀ i, ZMod (p i) → ℂ) (hg : ∀ i, g i 0 = 0) (D : ℕ) (v : ℤ)
    (hv : ¬ ∀ i, IsUnit (v : ZMod (p i))) :
    movingRegularTransform p g D v = 0 := by
…

Mentions: OAI.Ostmann.movingRegularTransform

theorem OAI.Ostmann.movingRegularTransform_unit_guard line 147

Source documentation

Inserting the exact initial unit guard changes no Fourier coefficient.

theorem movingRegularTransform_unit_guard {I : Type*} [Fintype I]
    (p : I → ℕ) [∀ i, Fact (p i).Prime]
    (g : ∀ i, ZMod (p i) → ℂ) (hg : ∀ i, g i 0 = 0) (D : ℕ) (v : ℤ) :
    (if ∀ i, IsUnit (v : ZMod (p i)) then movingRegularTransform p g D v else 0) =
      movingRegularTransform p g D v := by
…

Mentions: OAI.Ostmann.movingRegularTransform