HistogramScaleDecay.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform decay of the histogram and residue denominator losses

theorem OAI.JointDickman.channelMesh_scale_bound line 12

theorem OAI.JointDickman.histogram_residue_denominator_decay line 32

Source documentation

After summing denominators, both actual small losses still tend to zero, uniformly for eta*T <= j and the required polynomial modulus range.

theorem histogram_residue_denominator_decay
    (hMP : PublishedInputs.PrimeProductMertensInput) {η : ℝ} (hη : 0 < η) :
    ∃ ε : ℕ → ℝ, Tendsto ε atTop (𝓝 0) ∧
      ∀ m : ℕ, 0 < m → ∀ᶠ B : ℕ in atTop,
      ∀ (j Q : ℕ) (T : ℝ), 0 < j → 0 < Q → 0 ≤ T → η*T ≤ j → j*Q ≤ B^15 →
      (T/j)*kernelDenominatorSum j Q*
        ((B : ℝ)*channelMesh (channelFineCount m B)+(B : ℝ)^(-(1/200 : ℝ))) ≤ ε B := by
…

Mentions: OAI.JointDickman.PublishedInputs.PrimeProductMertensInput, OAI.JointDickman.kernelDenominatorSum, OAI.JointDickman.channelMesh, OAI.JointDickman.channelFineCount