MRTDivisorPairs.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The divisor-square estimate in the mixed prime/cofactor moment. The map (d,e) ↦ (gcd(d,e), d/gcd(d,e), e/gcd(d,e)) bounds a pair of supported divisors by three supported factors whose product divides the integer. Summing the divisibility tests gives a finite Euler majorant.

def OAI.TwoPointCorrelations.mrtGcdTriple line 16
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTDivisorPairs.lean:16 (same declaration text).
lemma OAI.TwoPointCorrelations.mrt_gcd_triple_left line 19
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTDivisorPairs.lean:19 (same declaration text).
lemma OAI.TwoPointCorrelations.mrt_gcd_triple_right line 23
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTDivisorPairs.lean:23 (same declaration text).
lemma OAI.TwoPointCorrelations.mrt_gcd_triple_injective line 27
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTDivisorPairs.lean:27 (same declaration text).
lemma OAI.TwoPointCorrelations.mrt_gcd_triple_product line 33
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTDivisorPairs.lean:33 (same declaration text).
theorem OAI.TwoPointCorrelations.mrt_divisor_pair_card line 47
Source documentation
A finite divisor-closed positive set suffices; no asymptotic sieve or mean-value theorem is hidden in the combinatorial estimate.
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTDivisorPairs.lean:47 (same declaration text).
```
theorem mrt_divisor_pair_card (S : Finset ℕ)
    (hS : ∀ d ∈ S, 0 < d)
    (hclosed : ∀ d ∈ S, ∀ e : ℕ, 0 < e → e ∣ d → e ∈ S) (n : ℕ) :
    ((S.filter (fun d => d ∣ n)).card) ^ 2 ≤
      ((S ×ˢ (S ×ˢ S)).filter (fun v => v.1 * (v.2.1 * v.2.2) ∣ n)).card := by
…
```
theorem OAI.TwoPointCorrelations.mrt_divisor_count_second_moment line 78
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTDivisorPairs.lean:78 (same declaration text).