OAI/NumberTheory/TwoPoint/Bounds/PaddingBinSquare.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The actual bin-square padding average is bounded by the exact difference small-ball probability, uniformly in a common translation of all bins.

  1. lemma OAI.TwoPointCorrelations.FiniteLaw.average_finset_sum line 19
  2. lemma OAI.TwoPointCorrelations.FiniteLaw.partial_collision_bound line 24
  3. def OAI.TwoPointCorrelations.paddingBin line 60
  4. lemma OAI.TwoPointCorrelations.paddingBin_difference line 62
  5. def OAI.TwoPointCorrelations.paddingBinMass line 69
  6. lemma OAI.TwoPointCorrelations.padding_bin_square_small_ball line 72
  7. theorem OAI.TwoPointCorrelations.ModFiveThetaInput.padding_bin_square line 104

    Source documentation

    The manuscript's squared bin mass, with tilted prime availability and actual independent divisor selections, is O(1/L) uniformly in bin location.

    theorem ModFiveThetaInput.padding_bin_square (hP : ModFiveThetaInput) (E : Finset ℕ) :
    ∃ C : ℝ, 0 < C ∧ ∀ (L η c : ℝ) (B : Finset ℤ), 1 ≤ L → 0 < η → η ≤ 1 →
      (paddingAvailableLaw (paddingPrimeSupply E L)
        (fun _ hp => (paddingPrimeSupply_prime hp).two_le)).average (fun a =>
          ∑ j ∈ B, (paddingBinMass (paddingPrimeSupply E L) a η c j) ^ 2) ≤ C / L := by
…

    Mentions: OAI.TwoPointCorrelations.ModFiveThetaInput, OAI.TwoPointCorrelations.paddingAvailableLaw, OAI.TwoPointCorrelations.paddingPrimeSupply, OAI.TwoPointCorrelations.paddingPrimeSupply_prime, OAI.TwoPointCorrelations.paddingBinMass