EndpointResiduePartition.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Exact residue decomposition of the endpoint exponential sums

theorem OAI.JointDickman.residue_nat_phase line 12

theorem OAI.JointDickman.endpoint_residue_partition line 21

Source documentation

The residue phase is kept exactly when integers are assigned to cells. Only the slowly varying archimedean factor is averaged later.

theorem endpoint_residue_partition {D : Type*} [Fintype D] [DecidableEq D]
    {B q : ℕ} [NeZero q] (lower upper : D → ℝ)
    (hdisjoint : ∀ d e s, s ∈ Set.Ioc (lower d) (upper d) →
      s ∈ Set.Ioc (lower e) (upper e) → d = e)
    (s : Finset ℕ) (J : Finset D) (c : ℕ → ℂ) (h : ZMod q) (ν : ℝ)
    (hsupp : ∀ n ∈ s, c n ≠ 0 → ∃ i ∈ J, ∃ r : (ZMod q)ˣ,
      logResidueCell B q lower upper n = some (i,r)) :
    (∑ n ∈ s, c n*additivePhase ((n : ℝ)*(h.val/(q : ℝ)+ν))) =
      unitResidueFourier (fun r => ∑ i ∈ J, ∑ n ∈ s,
        if logResidueCell B q lower upper n = some (i,r)
        then c n*additivePhase ((n : ℝ)*ν) else 0) h := by
…

Mentions: OAI.JointDickman.logResidueCell, OAI.JointDickman.additivePhase, OAI.JointDickman.unitResidueFourier