OAI/NumberTheory/Ostmann/Construction/UnitPrimeCellSupport.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.mem_unitPrimeCellSupport_iff line 10
2. theorem OAI.Ostmann.unitPrimeCellSupport_eq line 33

   Source documentation

   A modulus below every lower endpoint removes no original prime atom.

   theorem unitPrimeCellSupport_eq {C : Type*} [Fintype C]
       (q : ℕ) [NeZero q] (u v : C → ℝ) (hq : ∀ c, (q : ℝ) ≤ Real.exp (u c)) :
       primeCellSupport q (fun c : C × (ZMod q)ˣ => c.2.val.val)
         (fun c => u c.1) (fun c => v c.1) = primeCellSupport 1 (fun _ : C => 0) u v := by
   …

   Mentions: OAI.Ostmann.primeCellSupport

3. theorem OAI.Ostmann.unitPrimeCellLabel_lift line 51
4. theorem OAI.Ostmann.unitPrimeCells_separated line 64

   Source documentation

   Disjoint real cells and distinct unit residues give the required actual prime partition, independently of prime-distribution estimates.

   theorem unitPrimeCells_separated {C : Type*} [Fintype C]
       (q : ℕ) [NeZero q] (u v : C → ℝ)
       (hsep : ∀ c d, c ≠ d → v c ≤ u d ∨ v d ≤ u c) :
       ∀ c d : C × (ZMod q)ˣ, c ≠ d →
         ¬Nat.ModEq q c.2.val.val d.2.val.val ∨ v c.1 ≤ u d.1 ∨ v d.1 ≤ u c.1 := by
   …