MRTMultiplicativeReduction.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

The general-multiplicative reduction in corrected MRT §3. The completely multiplicative part keeps the original values at primes; the convolution correction vanishes at primes and is bounded by two at higher prime powers.

def OAI.TwoPointCorrelations.mrtCompletePart line 15
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTMultiplicativeReduction.lean:15 (same declaration text).
def OAI.TwoPointCorrelations.mrtCorrectionLocal line 18
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTMultiplicativeReduction.lean:18 (same declaration text).
def OAI.TwoPointCorrelations.mrtCorrection line 21
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTMultiplicativeReduction.lean:21 (same declaration text).
lemma OAI.TwoPointCorrelations.fromPrimePowers_prime_pow line 24
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTMultiplicativeReduction.lean:24 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtCompletePart_prime_pow line 31
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTMultiplicativeReduction.lean:31 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtCompletePart_mul line 35
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTMultiplicativeReduction.lean:35 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtCompletePart_oneBounded line 41
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTMultiplicativeReduction.lean:41 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtCorrectionLocal_zero line 48
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTMultiplicativeReduction.lean:48 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtCorrectionLocal_one line 52
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTMultiplicativeReduction.lean:52 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtCorrectionLocal_succ line 56
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTMultiplicativeReduction.lean:56 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtCorrection_prime_pow line 60
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTMultiplicativeReduction.lean:60 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtCorrectionLocal_norm_le line 64
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTMultiplicativeReduction.lean:64 (same declaration text).
lemma OAI.TwoPointCorrelations.mrt_local_convolution line 76
Source documentation
The local prime-power convolution telescopes exactly.
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTMultiplicativeReduction.lean:76 (same declaration text).
```
lemma mrt_local_convolution (f : ℕ → ℂ) (h1 : f 1 = 1) (p k : ℕ) :
    (∑ i ∈ range (k + 1), f p ^ i * mrtCorrectionLocal f p (k - i)) =
      f (p ^ k) := by
…
```
Mentions: OAI.TwoPointCorrelations.mrtCorrectionLocal
def OAI.TwoPointCorrelations.mrtArithmetic line 89
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTMultiplicativeReduction.lean:89 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtArithmetic_apply_pos line 92
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTMultiplicativeReduction.lean:92 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtArithmetic_isMultiplicative line 95
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTMultiplicativeReduction.lean:95 (same declaration text).
theorem OAI.TwoPointCorrelations.mrt_multiplicative_convolution line 107
Source documentation
Every normalized multiplicative function factors as g₁ * h, where g₁ is completely multiplicative and h(p)=0.
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTMultiplicativeReduction.lean:107 (same declaration text).
```
theorem mrt_multiplicative_convolution (f : ℕ → ℂ) (hf : Multiplicative f)
    (h1 : f 1 = 1) :
    mrtArithmetic (mrtCompletePart f) * mrtArithmetic (mrtCorrection f) =
      mrtArithmetic f := by
…
```
Mentions: OAI.TwoPointCorrelations.Multiplicative, OAI.TwoPointCorrelations.mrtArithmetic, OAI.TwoPointCorrelations.mrtCompletePart, OAI.TwoPointCorrelations.mrtCorrection
theorem OAI.TwoPointCorrelations.mrt_multiplicative_divisor_sum line 132
Source documentation
The convolution identity in the positive-integer notation used in MRT.
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTMultiplicativeReduction.lean:132 (same declaration text).
```
theorem mrt_multiplicative_divisor_sum (f : ℕ → ℂ) (hf : Multiplicative f)
    (h1 : f 1 = 1) {n : ℕ} (hn : 0 < n) :
    f n = ∑ d ∈ n.divisors, mrtCorrection f d * mrtCompletePart f (n / d) := by
…
```
Mentions: OAI.TwoPointCorrelations.Multiplicative, OAI.TwoPointCorrelations.mrtCorrection, OAI.TwoPointCorrelations.mrtCompletePart