PaddingDegreeTail.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The exact tilted padding law has mean at most 4 log L eventually. The finite exponential-moment bound gives the manuscript's L^-100 large-padding-degree error using the same fixed-modulus prime input.

lemma OAI.TwoPointCorrelations.paddingPrimeSupply_split line 16
lemma OAI.TwoPointCorrelations.paddingPrimeSupply_split_disjoint line 41
theorem OAI.TwoPointCorrelations.ModFiveThetaInput.padding_reciprocal_mass line 50
lemma OAI.TwoPointCorrelations.padding_mean_le_reciprocal line 62
theorem OAI.TwoPointCorrelations.ModFiveThetaInput.eventually_padding_mean line 73
theorem OAI.TwoPointCorrelations.ModFiveThetaInput.eventually_padding_degree_tail line 85

theorem OAI.TwoPointCorrelations.ModFiveThetaInput.eventually_padding_residue_degree_tail line 115

Source documentation

The original uniform-residue expectation, with its literal padding weight retained, has the same L^-100 degree-deletion bound.

theorem ModFiveThetaInput.eventually_padding_residue_degree_tail (hP : ModFiveThetaInput)
    (E : Finset ℕ) :
    ∀ᶠ L : ℝ in atTop, ∀ (B : ℕ) (n : ℤ)
      (hQB : ∀ p ∈ paddingPrimeSupply E L, p ≤ B),
      (FiniteLaw.independent (fun p : paddingPrimeSupply E L =>
        uniformResidueLaw B p.val (paddingPrimeSupply_prime p.property).pos
          (hQB p p.property))).average (fun z =>
            paddingTiltWeight _ (paddingResidueAvailable _ B n z) *
              if 400 * Real.log L < booleanCount (paddingResidueAvailable _ B n z)
              then 1 else 0) / paddingTiltNormalizer (paddingPrimeSupply E L) ≤ L ^ (-100 : ℝ) := by
…

Mentions: OAI.TwoPointCorrelations.ModFiveThetaInput, OAI.TwoPointCorrelations.paddingPrimeSupply, OAI.TwoPointCorrelations.FiniteLaw.independent, OAI.TwoPointCorrelations.uniformResidueLaw, OAI.TwoPointCorrelations.paddingPrimeSupply_prime, OAI.TwoPointCorrelations.paddingTiltWeight, OAI.TwoPointCorrelations.paddingResidueAvailable, OAI.TwoPointCorrelations.booleanCount, OAI.TwoPointCorrelations.paddingTiltNormalizer