PaddingResidueTilt.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

At every translated site of the uniform residue model, divisibility indicators give independent Bernoulli(1/p) variables. Thus the exact weighted residue expectation is the tilted padding law used in the bin-square bound.

def OAI.TwoPointCorrelations.paddingResidueAvailable line 17
lemma OAI.TwoPointCorrelations.padding_residue_single_law line 21
lemma OAI.TwoPointCorrelations.padding_residue_average line 39
lemma OAI.TwoPointCorrelations.padding_residue_tilt line 52
lemma OAI.TwoPointCorrelations.padding_residue_bin_square_le line 64

theorem OAI.TwoPointCorrelations.ModFiveThetaInput.padding_residue_bin_square line 81

Source documentation

Literal residue-model rho_j, weighted by w/S, satisfies the padding anti-concentration estimate uniformly in site and bin translation.

theorem ModFiveThetaInput.padding_residue_bin_square (hP : ModFiveThetaInput) (E : Finset ℕ) :
    ∃ C : ℝ, 0 < C ∧ ∀ (L η c : ℝ) (B : ℕ) (n : ℤ) (bins : Finset ℤ),
      1 ≤ L → 0 < η → η ≤ 1 →
      ∀ 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, (literalPaddingBinMass _ (paddingResidueAvailable _ B n z) η c j) ^ 2) /
                paddingTiltNormalizer (paddingPrimeSupply E L) ≤ C / L := 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.literalPaddingBinMass, OAI.TwoPointCorrelations.paddingTiltNormalizer