EndpointHistogramIdentity.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Exact endpoint-to-histogram identity on the actual grid

theorem OAI.JointDickman.channelCells_cover line 13
theorem OAI.JointDickman.primeSplitProductSupport_pos line 27
theorem OAI.JointDickman.primeSplitProductSupport_coprime line 32

theorem OAI.JointDickman.endpoint_histogram_identity line 45

Source documentation

With the full product support and the actual logarithmic cells, (38) is exactly a residue Fourier transform before any averaging of the test.

theorem endpoint_histogram_identity {m B q : ℕ} [NeZero q]
    (hm : 0 < m) (hB : 0 < B) (hcut : q ≤ auxiliaryCutoff B)
    {N : ℝ} (hN : 0 < N)
    (g : (auxiliaryPrimes B → Bool) → ℝ) (w : ℝ → ℝ) (h : ZMod q) (ν : ℝ)
    (hsupp : ∀ k ∈ primeSplitProductSupport (auxiliaryPrimes B), w (k/N) ≠ 0 →
      Real.log k/B ∈ Set.Ioc (1/2 : ℝ) 3) :
    (∑ k ∈ primeSplitProductSupport (auxiliaryPrimes B),
      (signedSplitProductMass (auxiliaryPrimes B) (subsetSiteTest (auxiliaryPrimes B) g) k*w (k/N) : ℝ)*
        additivePhase ((k : ℝ)*(h.val/(q : ℝ)+ν))) =
      unitResidueFourier (fun r => ∑ i : Fin (channelFineCount m B),
        manuscriptCellSum m B q g (logOscillatoryTest w B N (ν*N)) i r) h := by
…

Mentions: OAI.JointDickman.auxiliaryCutoff, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.primeSplitProductSupport, OAI.JointDickman.signedSplitProductMass, OAI.JointDickman.subsetSiteTest, OAI.JointDickman.additivePhase, OAI.JointDickman.unitResidueFourier, OAI.JointDickman.channelFineCount, OAI.JointDickman.manuscriptCellSum, OAI.JointDickman.logOscillatoryTest