HistogramResidueProjection.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Residue projection in the actual finite histogram

theorem OAI.JointDickman.histogram_cell_vector_bound line 12

Source documentation

Finite form of (39) for a signed cell vector and arbitrary complex tests.

theorem histogram_cell_vector_bound {ι : Type*} [DecidableEq ι]
    {q : ℕ} [NeZero q] (J : Finset ι) {δ M : ℝ}
    (hδ : 0 ≤ δ) (hM : 0 ≤ M) (U : ι → (ZMod q)ˣ → ℝ)
    (F : ι → ℂ) (hF : ∀ i ∈ J, ‖F i‖ ≤ M) :
    (∑ h : ZMod q, ‖unitResidueFourier
      (fun r => ∑ i ∈ J, (δ : ℂ)*(U i r : ℂ)*F i) h/(q.totient : ℂ)‖^2) ≤
      ((q : ℝ)/(q.totient : ℝ))*((J.card : ℝ)*δ)*M^2*
        (∑ i ∈ J, ∑ r : (ZMod q)ˣ, (δ/(q.totient : ℝ))*U i r^2) := by
…

Mentions: OAI.JointDickman.unitResidueFourier

theorem OAI.JointDickman.manuscript_histogram_residue_projection line 36

Source documentation

The residue-dependent part of the manuscript channel is controlled by its proved squared residue norm, on any selected collection of cells.

theorem manuscript_histogram_residue_projection {m B q : ℕ} [NeZero q]
    (hm : 0 < m) (hB : 0 < B) (J : Finset (Fin (channelFineCount m B)))
    (g : (auxiliaryPrimes B → Bool) → ℝ) (F : Fin (channelFineCount m B) → ℂ)
    {M : ℝ} (hM : 0 ≤ M) (hF : ∀ i ∈ J, ‖F i‖ ≤ M) :
    (∑ h : ZMod q, ‖unitResidueFourier
      (fun r => ∑ i ∈ J, (channelMesh (channelFineCount m B) : ℂ)*
        ((manuscriptChannel m B q g (i,r)-
          finiteResidueAverage (fun s => manuscriptChannel m B q g (i,s))) : ℝ)*F i)
      h/(q.totient : ℂ)‖^2) ≤
      ((q : ℝ)/(q.totient : ℝ))*((J.card : ℝ)*channelMesh (channelFineCount m B))*M^2*
        (∑ i ∈ J, ∑ r : (ZMod q)ˣ,
          (channelMesh (channelFineCount m B)/(q.totient : ℝ))*
…

Mentions: OAI.JointDickman.channelFineCount, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.unitResidueFourier, OAI.JointDickman.channelMesh, OAI.JointDickman.manuscriptChannel, OAI.JointDickman.finiteResidueAverage

theorem OAI.JointDickman.manuscript_histogram_residue_projection_rate line 54

Source documentation

Summing disjoint local squared errors is bounded by the global channel residue norm. The only arithmetic inputs are the published channel inputs.

theorem manuscript_histogram_residue_projection_rate
    (hSD : PublishedInputs.SquarefreeSelbergDelangeInput)
    (hSW : PublishedInputs.SquarefreeCharacterEstimateInput)
    (hM : PublishedInputs.PrimeReciprocalMertensInput)
    (hMP : PublishedInputs.PrimeProductMertensInput) :
    ∃ K : ℝ, 0 < K ∧ ∀ m : ℕ, 0 < m → ∀ᶠ B : ℕ in Filter.atTop,
      ∀ q : ℕ, [NeZero q] → q ≤ B →
      ∀ J : Finset (Fin (channelFineCount m B)),
      ∀ g : (auxiliaryPrimes B → Bool) → ℝ,
      ∀ (F : Fin (channelFineCount m B) → ℂ) (M : ℝ), 0 ≤ M →
      (∀ i ∈ J, ‖F i‖ ≤ M) →
      (∑ h : ZMod q, ‖unitResidueFourier
…

Mentions: OAI.JointDickman.PublishedInputs.SquarefreeSelbergDelangeInput, OAI.JointDickman.PublishedInputs.SquarefreeCharacterEstimateInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.PublishedInputs.PrimeProductMertensInput, OAI.JointDickman.channelFineCount, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.unitResidueFourier