LeanPool.DeadEnds.CRT #
The modulus M = ∏_{p ∈ S} p²
Equations
- LeanPool.DeadEnds.primeSquareProduct S = ∏ p ∈ S, ↑p ^ 2
Instances For
Valid residues mod M: residues r such that for all p ∈ S, r mod p² is valid
Equations
- LeanPool.DeadEnds.validResiduesMod b T S = {r ∈ Finset.range (LeanPool.DeadEnds.primeSquareProduct S) | ∀ p ∈ S, ¬↑p ^ 2 ∣ r ∧ ∀ d ∈ T, ¬↑p ^ 2 ∣ b * r + d}
Instances For
The product of local density factors L = ∏_{p ∈ S} localDensityFactor p b T
Equations
- LeanPool.DeadEnds.localDensityProduct b T S = ∏ p ∈ S, LeanPool.DeadEnds.localDensityFactor (↑p) b T
Instances For
The local valid residues for a single prime p: residues r in [0, p²) such that p² ∤ r and for all d ∈ T, p² ∤ (b * r + d).
Equations
Instances For
The list S.toList satisfies pairwise coprimality for the map p ↦ p².
Uses pairwise_coprime_prime_squares and transfers the set pairwise property to the list.
Mathlib's List.pairwise_of_reflexive_of_forall_ne handles this for symmetric reflexive
relations,
but coprimality is not reflexive (unless p² = 1). Instead we use the fact that S.toList.Nodup
and the set pairwise property directly imply the list pairwise property.
Specifically, uses List.Nodup.pairwise_of_set_pairwise : l.Nodup → {x | x ∈ l}.Pairwise r → List.Pairwise r l
together with Finset.nodup_toList : ∀ (s : Finset α), s.toList.Nodup and
Finset.coe_toList : ↑s.toList = ↑s (as sets).
Congruence modulo each prime-square factor implies congruence modulo their product.
The CRT remainder map is injective on residues below the product modulus.
For any prime p, p² ≠ 0.
This is needed to apply Nat.chineseRemainderOfFinset.
Uses Nat.Prime.pos : ∀ {p : ℕ}, Nat.Prime p → 0 < p and
pow_ne_zero : ∀ {M₀ : Type u_1} [inst : MonoidWithZero M₀] {a : M₀} [NoZeroDivisors M₀] (n : ℕ), a ≠ 0 → a ^ n ≠ 0.
Valid residue counts factor as the product of local valid residue counts.
A finite product of local density factors is at most one.