OAI/NumberTheory/Ostmann/Construction/FrozenInitialSpectatorData.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.frozenInitialSpectatorPrimes line 9
2. theorem OAI.Ostmann.frozenInitialSpectatorPrimes_injective line 12
3. theorem OAI.Ostmann.frozenInitialSpectatorPrimes_mem line 17
4. structure OAI.Ostmann.FrozenInitialSpectatorData line 26

   Source documentation

   This packages consequences of the selected support, without selecting another family.

   structure FrozenInitialSpectatorData (A : Set ℕ) (N : ℕ) {d : ℕ}
       (p : Fin (d + d) → ℕ) (L ε : ℝ) (cutoff : ℕ) (D : Finset ℕ) : Prop where
   …

5. theorem OAI.Ostmann.frozen_initial_spectator_data line 42
6. theorem OAI.Ostmann.FrozenInitialSpectatorData.comparison_upper line 77
7. theorem OAI.Ostmann.FrozenInitialSpectatorData.mono line 83