SampledKernelInversion.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Exact inversion of the sampled, residue-averaged arithmetic kernel

theorem OAI.JointDickman.projected_residue_full_integral line 13
theorem OAI.JointDickman.sampledProjectedValue_fourier_inversion line 38

theorem OAI.JointDickman.sampledProjectedFourier_kernel line 60

Source documentation

The sampled archimedean kernel and the exact singular-series coefficient. The residue condition remains the one in the lifted major-arc partition.

theorem sampledProjectedFourier_kernel (m B j q : ℕ) [NeZero j] [NeZero q] [NeZero (j*q)]
    (J K : Finset (Fin (channelFineCount m B)))
    (g h : (auxiliaryPrimes B → Bool) → ℝ)
    (a b : Fin (channelFineCount m B) → ℂ)
    (x y : Fin (channelFineCount m B) → ℝ) (w : 𝓢(ℝ,ℝ)) :
    ((μ q : ℂ)/(q.totient : ℂ))*(∑ r : ZMod (j*q), if r.val.Coprime q then
      ∫ ξ : ℝ, testFourierTransform w ξ*
        sampledProjectedFourier m B (j*q) J g (fun i => a i*additivePhase (ξ*x i)) r*
        sampledProjectedFourier m B (j*q) K h (fun i => b i*additivePhase (-ξ*y i)) (-r)
      else 0) =
      (((j : ℝ)/j.totient*singularSeriesCoefficient j q : ℝ) : ℂ)*
        ∑ i ∈ J, ∑ k ∈ K,
…

Mentions: OAI.JointDickman.channelFineCount, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.testFourierTransform, OAI.JointDickman.sampledProjectedFourier, OAI.JointDickman.additivePhase, OAI.JointDickman.singularSeriesCoefficient