PageConductorProjection.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The selected Page correction factors through the frequency modulus

theorem OAI.Ostmann.pageAtModulus_mul_eq line 14

Source documentation

After excluding a selected large conductor prime, the correction on the full modulus is exactly its correction on the frequency modulus.

theorem pageAtModulus_mul_eq (z : Option PrimitiveRealZero) (Q R T : ℕ)
    (hQ : ∀ p, p.Prime → p ∣ Q → p < T)
    (hR : ∀ p, p.Prime → p ∣ R → T ≤ p)
    (hexcluded : ∀ e, z = some e → ∀ p,
      deletedConductorPrime e.modulus T = some p → ¬p ∣ R) :
    pageAtModulus (Q * R) z = pageAtModulus Q z := by
…

Mentions: OAI.Ostmann.PrimitiveRealZero, OAI.Ostmann.deletedConductorPrime, OAI.Ostmann.pageAtModulus

theorem OAI.Ostmann.pageCoefficient_eq_of_modEq line 33
Source documentation
The character value itself depends only on the smaller residue. This is the arithmetic justification for keeping the Page factor in the frequency-coordinate average when applying CRT.
```
theorem pageCoefficient_eq_of_modEq (z : Option PrimitiveRealZero) {Q a b : ℕ}
    (hab : Nat.ModEq Q a b) :
    pageCoefficient (pageAtModulus Q z) a = pageCoefficient (pageAtModulus Q z) b := by
…
```
Mentions: OAI.Ostmann.PrimitiveRealZero, OAI.Ostmann.pageCoefficient, OAI.Ostmann.pageAtModulus
theorem OAI.Ostmann.selectedPageCorrection_frequency line 45