CoarseCompactness.lean`

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform coarse compactness of the manuscript channel

theorem OAI.JointDickman.exists_small_coarse_cutoff line 12
theorem OAI.JointDickman.groupedManuscriptChannel_coarse_compactness line 33
Source documentation
The coarse partition is fixed before B grows and works uniformly for all real input functions, including inputs depending on B.
```
theorem groupedManuscriptChannel_coarse_compactness
    (hSD : PublishedInputs.SquarefreeSelbergDelangeInput)
    (hSW : PublishedInputs.SquarefreeCharacterEstimateInput)
    (hM : PublishedInputs.PrimeReciprocalMertensInput)
    (hMP : PublishedInputs.PrimeProductMertensInput)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ m : ℕ, 0 < m ∧ ∀ᶠ B : ℕ in atTop,
      ∀ f : (auxiliaryPrimes B → Bool) → ℝ,
      (∑ a : Fin m × Fin (channelBlockCount m B), channelMesh (channelFineCount m B) *
        (groupedManuscriptChannel m B f a -
          finiteResidueAverage (fun r => groupedManuscriptChannel m B f (a.1, r))) ^ 2) ≤
        ε * ∑ x, fullPrimeMass (auxiliaryPrimes B) x * f x ^ 2 := by
…
```
Mentions: OAI.JointDickman.PublishedInputs.SquarefreeSelbergDelangeInput, OAI.JointDickman.PublishedInputs.SquarefreeCharacterEstimateInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.PublishedInputs.PrimeProductMertensInput, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.channelBlockCount, OAI.JointDickman.channelMesh, OAI.JointDickman.channelFineCount, OAI.JointDickman.groupedManuscriptChannel, OAI.JointDickman.finiteResidueAverage, OAI.JointDickman.fullPrimeMass