OAI/NumberTheory/Ostmann/Construction/IntegerGridSupport.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.integerLogCellSet line 17
2. theorem OAI.Ostmann.integerLogCellSet_disjoint line 21
3. def OAI.Ostmann.integerCellSupport line 35
4. def OAI.Ostmann.integerCellLabel line 39
5. theorem OAI.Ostmann.integerCellLabel_mem line 43
6. theorem OAI.Ostmann.integerCellLabel_fiber line 55
7. def OAI.Ostmann.buildIntegerCellPartition line 80

   Source documentation

   A fully constructed partition of the actual integers in the selected log cells. Separation is a numerical/residue property, not an assertion about the distribution of integers.

   noncomputable def buildIntegerCellPartition {C : Type*} [Fintype C]
       (q : ℕ) (hq : 0 < q) (a : C → ℕ) (s t : C → ℝ) (c₀ : C)
       (hst : ∀ c, s c ≤ t c) (hshort : ∀ c, t c ≤ s c + 1)
       (hsep : ∀ c d, c ≠ d → ¬Nat.ModEq q (a c) (a d) ∨ t c ≤ s d ∨ t d ≤ s c) :
       IntegerCellPartition (integerCellSupport q a s t) C where
   …

   Mentions: OAI.Ostmann.IntegerCellPartition, OAI.Ostmann.integerCellSupport

8. def OAI.Ostmann.integerGridLower line 95
9. def OAI.Ostmann.integerGridUpper line 98
10. theorem OAI.Ostmann.integerGrid_separated line 101
11. def OAI.Ostmann.gridIntegerCellPartition line 125
12. theorem OAI.Ostmann.mem_integerLogCellSet_iff line 137
13. theorem OAI.Ostmann.mem_gridIntegerSupport_iff line 154

    Source documentation

    All residue classes are used for the external giant. The constructed support is exactly the original interval of positive integers.

    theorem mem_gridIntegerSupport_iff (N q : ℕ) [NeZero q] (s h : ℝ) (hh : 0 ≤ h) (n : ℕ) :
        n ∈ integerCellSupport q (fun c : Fin N × ZMod q => c.2.val)
          (integerGridLower s h) (integerGridUpper s h) ↔
          0 < n ∧ Real.log (n : ℝ) ∈ Set.Ioc s (s + N * h) := by
    …

    Mentions: OAI.Ostmann.integerCellSupport, OAI.Ostmann.integerGridLower, OAI.Ostmann.integerGridUpper