ConductorDeletion.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Conductor support after deleting one large prime

For each exceptional conductor choose one prime divisor above the threshold, if there is one, and exclude that value from the nongiant priors. A conductor that still divides the arithmetic modulus is then supported on its frequency block, with full prime-power multiplicity.

def OAI.Ostmann.deletedConductorPrime line 19
theorem OAI.Ostmann.deletedConductorPrime_spec line 22
theorem OAI.Ostmann.conductor_dvd_frequency_of_deletion line 34
Source documentation
If the chosen large divisor was excluded, any surviving conductor divides only the small frequency modulus. No squarefree assumption on the conductor or on either modulus is needed.
```
theorem conductor_dvd_frequency_of_deletion (D Q R T : ℕ)
    (hQ : ∀ p, p.Prime → p ∣ Q → p < T)
    (hR : ∀ p, p.Prime → p ∣ R → T ≤ p)
    (hdeleted : ∀ p, deletedConductorPrime D T = some p → ¬p ∣ R)
    (hD : D ∣ Q * R) : D ∣ Q := by
…
```
Mentions: OAI.Ostmann.deletedConductorPrime
theorem OAI.Ostmann.excluded_prime_not_dvd_product line 53
Source documentation
Excluding a prime value excludes it from a product of powers of sampled primes, even when the occurrence exponents exceed one.
```
theorem excluded_prime_not_dvd_product {p : ℕ} (hp : p.Prime)
    (P : Finset ℕ) (e : ℕ → ℕ) (hP : ∀ q ∈ P, q.Prime) (hex : p ∉ P) :
    ¬p ∣ ∏ q ∈ P, q ^ e q := by
…
```