PageSelection.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

A single exceptional character for every modulus in a row

Only zeros in Page's common region are retained. Local exceptional zeros outside that region will be bounded as an error, rather than identified with a character belonging to a different modulus.

def OAI.Ostmann.selectedPageZero line 16
def OAI.Ostmann.pageAtModulus line 21
theorem OAI.Ostmann.selectedPageZero_spec line 25
theorem OAI.Ostmann.selectedPageZero_eq line 35
theorem OAI.Ostmann.page_region_mono line 45
theorem OAI.Ostmann.localZero_eq_of_selected line 56
theorem OAI.Ostmann.localZero_selected_alternative line 66
Source documentation
Every local correction either equals the restriction of the same global Page correction, or is a zero lying strictly outside the common region. In the latter case the global correction is absent from that modulus.
```
theorem localZero_selected_alternative (P : PublishedProgressionInput) {q Q : ℕ}
    (hQ : 2 ≤ Q) (hq : 1 ≤ q) (hqQ : q ≤ Q) :
    P.localZero q = pageAtModulus q (selectedPageZero P Q) ∨
      ∃ e : PrimitiveRealZero, P.localZero q = some e ∧
        e.beta < 1 - P.kappa / Real.log (4 * (Q : ℝ)) ∧
        pageAtModulus q (selectedPageZero P Q) = none := by
…
```
Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.pageAtModulus, OAI.Ostmann.selectedPageZero, OAI.Ostmann.PrimitiveRealZero