PaddingLargeBinCut.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The squared-bin estimate gives the exact O(1/K) cost of deleting bins whose padding density exceeds K/L.

lemma OAI.TwoPointCorrelations.large_nonnegative_value line 13
lemma OAI.TwoPointCorrelations.FiniteLaw.large_bin_cut line 23
lemma OAI.TwoPointCorrelations.paddingBinMass_nonneg line 40

theorem OAI.TwoPointCorrelations.ModFiveThetaInput.padding_large_bin_cut line 44

Source documentation

Uniform over bin translations and every finite collection of bins.

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

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

theorem OAI.TwoPointCorrelations.ModFiveThetaInput.padding_residue_large_bin_cut line 64

Source documentation

The same bound in the original weighted uniform-residue expectation.

theorem ModFiveThetaInput.padding_residue_large_bin_cut (hP : ModFiveThetaInput)
    (E : Finset ℕ) :
    ∃ C : ℝ, 0 < C ∧ ∀ (L η c K : ℝ) (B : ℕ) (n : ℤ) (bins : Finset ℤ),
      1 ≤ L → 0 < η → η ≤ 1 → 0 < K →
      ∀ 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) *
              ∑ j ∈ bins,
                if K / L < literalPaddingBinMass _ (paddingResidueAvailable _ B n z) η c j
                then literalPaddingBinMass _ (paddingResidueAvailable _ B n z) η c j else 0) /
…

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.literalPaddingBinMass