MRTTypicalOutside.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Multiplication outside the selected prime bands preserves the typical mask. The resulting identity uses the unmasked factor on the left: the typical coefficient itself need not be multiplicative. In particular, the complete part can be extracted at every power of an outside prime, without a coprimality condition on the remaining argument.

lemma OAI.TwoPointCorrelations.mrtPrimeAvoids_prime_outside line 17
lemma OAI.TwoPointCorrelations.mrtPrimeAvoids_pow line 24

theorem OAI.TwoPointCorrelations.mrtTypicalCoefficient_mul_of_avoids line 37

Source documentation

Extract an avoiding factor from a completely multiplicative coefficient, while keeping the same typical mask on the cofactor.

theorem mrtTypicalCoefficient_mul_of_avoids {ι : Type*} (J : Finset ι)
    (P : ι → Finset ℕ) (hP : ∀ j ∈ J, ∀ p ∈ P j, p.Prime)
    (F : ℕ → ℂ)
    (hF : ∀ a b, 0 < a → 0 < b → F (a * b) = F a * F b)
    {d n : ℕ} (hd : 0 < d) (hn : 0 < n)
    (havoid : mrtPrimeAvoids (J.biUnion P) d) :
    mrtTypicalCoefficient J P F (d * n) = F d * mrtTypicalCoefficient J P F n := by
…

Mentions: OAI.TwoPointCorrelations.mrtPrimeAvoids, OAI.TwoPointCorrelations.mrtTypicalCoefficient

theorem OAI.TwoPointCorrelations.mrtTypicalComplete_mul_of_avoids line 50

theorem OAI.TwoPointCorrelations.mrtTypicalComplete_prime_pow_outside line 61

Source documentation

Prime powers outside the bands can be extracted even when the prime also divides the cofactor.

theorem mrtTypicalComplete_prime_pow_outside {ι : Type*} (J : Finset ι)
    (P : ι → Finset ℕ) (hP : ∀ j ∈ J, ∀ q ∈ P j, q.Prime)
    (F : ℕ → ℂ) {p : ℕ} (hp : p.Prime) (hpout : p ∉ J.biUnion P)
    (k n : ℕ) (hn : 0 < n) :
    mrtTypicalCoefficient J P (mrtCompletePart F) (p ^ k * n) =
      F p ^ k * mrtTypicalCoefficient J P (mrtCompletePart F) n := by
…

Mentions: OAI.TwoPointCorrelations.mrtTypicalCoefficient, OAI.TwoPointCorrelations.mrtCompletePart

theorem OAI.TwoPointCorrelations.mrtTypicalComplete_prime_pow_above line 77

Source documentation

A real upper endpoint for all selected bands discharges the outside condition used in the truncated prime convolution.

theorem mrtTypicalComplete_prime_pow_above {ι : Type*} (J : Finset ι)
    (P : ι → Finset ℕ) (hP : ∀ j ∈ J, ∀ q ∈ P j, q.Prime)
    {U : ℝ} (hupper : ∀ j ∈ J, ∀ q ∈ P j, (q : ℝ) ≤ U)
    (F : ℕ → ℂ) {p : ℕ} (hp : p.Prime) (hUp : U < (p : ℝ))
    (k n : ℕ) (hn : 0 < n) :
    mrtTypicalCoefficient J P (mrtCompletePart F) (p ^ k * n) =
      F p ^ k * mrtTypicalCoefficient J P (mrtCompletePart F) n := by
…

Mentions: OAI.TwoPointCorrelations.mrtTypicalCoefficient, OAI.TwoPointCorrelations.mrtCompletePart