OAI/NumberTheory/Ostmann/Construction/LogCellFamilyWindow.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Complete integer cell families around a real prime block

  1. def OAI.Ostmann.logBlockCenters line 11
  2. theorem OAI.Ostmann.logBlockCenters_bounds line 14
  3. theorem OAI.Ostmann.logCellFamilyWeight_le_one line 21
  4. theorem OAI.Ostmann.logBlockCenters_partition line 42
  5. theorem OAI.Ostmann.logBlockCenters_weight_zero line 59
  6. theorem OAI.Ostmann.logBlockCenters_full_cells line 71

    Source documentation

    One ambient giant container contains every complete cell in the block.

    theorem logBlockCenters_full_cells (lo hi : ℝ) :
    ∀ n ∈ logBlockCenters lo hi,
      smoothGiantPrimeRange n ⊆ smoothGiantPrimeRange (hi + 2) := by
…

    Mentions: OAI.Ostmann.logBlockCenters, OAI.Ostmann.smoothGiantPrimeRange