OriginalBulkResidues.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Separating the real cells and residues of the original prime sample

theorem OAI.Ostmann.sum_joint_cells_residues line 12

theorem OAI.Ostmann.original_bulk_residue_expansion line 22

Source documentation

Each actual prime tuple selects its own residue kernel. The left side is precisely the joint box/residue sum to which the Page comparison is applied.

theorem original_bulk_residue_expansion {J C : Type*} [Fintype J] [Fintype C]
    (P : Finset ℕ) (M : ℕ) [NeZero M] (u v : J → C → ℝ)
    (c₀ : C × (ZMod M)ˣ)
    (hP : ∀ j, primeCellSupport M (fun c : C × (ZMod M)ˣ => c.2.val.val)
      (fun c => u j c.1) (fun c => v j c.1) ⊆ P)
    (hsep : ∀ j (c d : C × (ZMod M)ˣ), c ≠ d →
      ¬Nat.ModEq M c.2.val.val d.2.val.val ∨ v j c.1 ≤ u j d.1 ∨ v j d.1 ≤ u j c.1)
    (f : (J → C) → (J → (ZMod M)ˣ) → BulkIntegrand J) :
    let S := fun j => primeCellSupport M (fun c : C × (ZMod M)ˣ => c.2.val.val)
…

Mentions: OAI.Ostmann.primeCellSupport, OAI.Ostmann.BulkIntegrand