OAI/NumberTheory/TwoPointCorrelations/PaddingCharacteristic.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The finite characteristic product in the padding argument. The loss from replacing p+4 by p is bounded explicitly by a convergent square sum.

  1. def OAI.TwoPointCorrelations.paddingCharacteristicFactor line 15

    Also declared: OAI/NumberTheory/TwoPoint/Bounds/PaddingCharacteristic.lean:15 (same declaration text).

  2. def OAI.TwoPointCorrelations.paddingCharacteristic line 18

    Also declared: OAI/NumberTheory/TwoPoint/Bounds/PaddingCharacteristic.lean:18 (same declaration text).

  3. def OAI.TwoPointCorrelations.paddingOscillation line 21

    Also declared: OAI/NumberTheory/TwoPoint/Bounds/PaddingCharacteristic.lean:21 (same declaration text).

  4. lemma OAI.TwoPointCorrelations.one_sub_cos_bounds line 24

    Also declared: OAI/NumberTheory/TwoPoint/Bounds/PaddingCharacteristic.lean:24 (same declaration text).

  5. lemma OAI.TwoPointCorrelations.paddingCharacteristicFactor_bounds line 27

    Also declared: OAI/NumberTheory/TwoPoint/Bounds/PaddingCharacteristic.lean:27 (same declaration text).

  6. lemma OAI.TwoPointCorrelations.padding_reciprocal_shift line 42

    Also declared: OAI/NumberTheory/TwoPoint/Bounds/PaddingCharacteristic.lean:42 (same declaration text).

  7. theorem OAI.TwoPointCorrelations.paddingCharacteristic_nonneg line 49

    Also declared: OAI/NumberTheory/TwoPoint/Bounds/PaddingCharacteristic.lean:49 (same declaration text).

  8. theorem OAI.TwoPointCorrelations.paddingCharacteristic_exp_bound line 53

    Also declared: OAI/NumberTheory/TwoPoint/Bounds/PaddingCharacteristic.lean:53 (same declaration text).

  9. theorem OAI.TwoPointCorrelations.paddingCharacteristic_power_bound line 89

    Source documentation

    Once the internally derived oscillatory prime estimate is supplied, the padding Fourier decay has the exponent 6/5 required for integrability.

    Also declared: OAI/NumberTheory/TwoPoint/Bounds/PaddingCharacteristic.lean:89 (same declaration text).

    theorem paddingCharacteristic_power_bound (Q : Finset ℕ) (hQ : ∀ p ∈ Q, 2 ≤ p)
    (L C t : ℝ) (hL : 0 ≤ L)
    (hprime : (3 / 4 : ℝ) * Real.log (1 + L * |t|) - C ≤ paddingOscillation Q t) :
    paddingCharacteristic Q t ≤ Real.exp ((8 / 5 : ℝ) * C + 64 / 5) *
      (1 + L * |t|) ^ (-6 / 5 : ℝ) := by
…

    Mentions: OAI.TwoPointCorrelations.paddingOscillation, OAI.TwoPointCorrelations.paddingCharacteristic