OAI/NumberTheory/TwoPointCorrelations/HalaszUnitCorrection.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The exact convolution with the constant-one function used for the near-twist renormalization. Its prime coefficients are the actual deviation from one, including missing-prime masks.

  1. def OAI.TwoPointCorrelations.halaszUnitCorrectionLocal line 15

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszUnitCorrection.lean:15 (same declaration text).

  2. def OAI.TwoPointCorrelations.halaszUnitCorrection line 18

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszUnitCorrection.lean:18 (same declaration text).

  3. lemma OAI.TwoPointCorrelations.halaszUnitCorrectionLocal_zero line 21

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszUnitCorrection.lean:21 (same declaration text).

  4. lemma OAI.TwoPointCorrelations.halaszUnitCorrectionLocal_succ line 24

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszUnitCorrection.lean:24 (same declaration text).

  5. lemma OAI.TwoPointCorrelations.halasz_unit_correction_prime_pow line 28

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszUnitCorrection.lean:28 (same declaration text).

  6. lemma OAI.TwoPointCorrelations.halasz_unit_correction_prime line 32

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszUnitCorrection.lean:32 (same declaration text).

  7. lemma OAI.TwoPointCorrelations.halasz_unit_correction_local_sum line 36

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszUnitCorrection.lean:36 (same declaration text).

  8. lemma OAI.TwoPointCorrelations.halasz_unit_correction_convolution line 44

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszUnitCorrection.lean:44 (same declaration text).

  9. lemma OAI.TwoPointCorrelations.halasz_unit_correction_divisor_sum line 68

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszUnitCorrection.lean:68 (same declaration text).

  10. lemma OAI.TwoPointCorrelations.halasz_unit_correction_local_bound line 84

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszUnitCorrection.lean:84 (same declaration text).

  11. lemma OAI.TwoPointCorrelations.halasz_unit_correction_prefix line 92

    Source documentation

    Exact prefix hyperbola identity.

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszUnitCorrection.lean:92 (same declaration text).

    lemma halasz_unit_correction_prefix (F : ℕ → ℂ) (hF : Multiplicative F)
    (hF1 : F 1 = 1) (N : ℕ) :
    (∑ n ∈ Icc 1 N, F n) =
      ∑ d ∈ Icc 1 N, (N / d : ℕ) * halaszUnitCorrection F d := by
…

    Mentions: OAI.TwoPointCorrelations.Multiplicative, OAI.TwoPointCorrelations.halaszUnitCorrection