OAI/NumberTheory/TwoPoint/Bounds/ActualPaddingIntegerBounds.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TwoPointCorrelations.uniformAverage_pi_product line 15

   Distinct definitions of this name: OAI/NumberTheory/TwoPoint/Bounds/PrimeDefectCRT.lean:14 (different declaration text). Qualify references as OAI.TwoPointCorrelations.uniformAverage_pi_product@path.

2. lemma OAI.TwoPointCorrelations.uniformAverage_padding_factor line 22
3. def OAI.TwoPointCorrelations.primeStateTruncatedWeight line 36
4. lemma OAI.TwoPointCorrelations.activeState_five_pow line 41
5. lemma OAI.TwoPointCorrelations.primeStateTruncatedWeight_average_le line 46
6. lemma OAI.TwoPointCorrelations.padding_state_coefficient_bound line 69
7. theorem OAI.TwoPointCorrelations.BravermanDepth22Input.eventually_prime_state_weight line 85
8. lemma OAI.TwoPointCorrelations.primeStateTruncatedWeight_actual line 131
9. lemma OAI.TwoPointCorrelations.primeSet_card_le_exp line 143
10. lemma OAI.TwoPointCorrelations.paddingTiltNormalizer_one_le line 154
11. theorem OAI.TwoPointCorrelations.BravermanDepth22Input.eventually_actual_padding_weight line 166

    Source documentation

    The manuscript's truncated-weight estimate, for literal integer sites and every permitted interval and offset.

    theorem BravermanDepth22Input.eventually_actual_padding_weight (hBr : BravermanDepth22Input) :
        ∃ A : ℕ, 1000 ≤ A ∧ ∀ᶠ L : ℝ in atTop,
          ∀ (Q : Finset ℕ), (∀ p ∈ Q, p.Prime) →
          (∀ p ∈ Q, (p : ℝ) ≤ Real.exp L) →
          ∀ (site : ℤ) (a N : ℕ), Real.exp (L ^ A / 2) ≤ (N : ℝ) →
          let T := uniformAverage (fun x : Fin N =>
    …

    Mentions: OAI.TwoPointCorrelations.BravermanDepth22Input, OAI.TwoPointCorrelations.uniformAverage

12. theorem OAI.TwoPointCorrelations.BravermanDepth22Input.eventually_actual_padding_weight_sum line 239

    Source documentation

    Summing over any fixed finite collection of offsets costs its cardinality.

    theorem BravermanDepth22Input.eventually_actual_padding_weight_sum
        (hBr : BravermanDepth22Input) :
        ∃ A : ℕ, 1000 ≤ A ∧ ∀ᶠ L : ℝ in atTop,
          ∀ (Q : Finset ℕ), (∀ p ∈ Q, p.Prime) →
          (∀ p ∈ Q, (p : ℝ) ≤ Real.exp L) →
          ∀ {ι : Type*} [DecidableEq ι] (offsets : Finset ι) (site : ι → ℤ)
            (a N : ℕ), Real.exp (L ^ A / 2) ≤ (N : ℝ) →
          (∑ i ∈ offsets, uniformAverage (fun x : Fin N =>
            (actualPaddingVertex Q (((a + x.val : ℕ) : ℤ) + site i)) ^ 2 *
              if actualPaddingDegreeCut Q L (((a + x.val : ℕ) : ℤ) + site i)
                then 1 else 0)) ≤
            2 * (offsets.card : ℝ) * paddingTiltNormalizer Q := by
    …

    Mentions: OAI.TwoPointCorrelations.BravermanDepth22Input, OAI.TwoPointCorrelations.uniformAverage, OAI.TwoPointCorrelations.actualPaddingVertex, OAI.TwoPointCorrelations.actualPaddingDegreeCut, OAI.TwoPointCorrelations.paddingTiltNormalizer