OriginalPrimeCellExpansion.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Residue-dependent kernels under the exact original prime law

theorem OAI.Ostmann.primeSubsetPrior_cell_atom line 12
theorem OAI.Ostmann.sum_coordinate_delta line 25

theorem OAI.Ostmann.original_prime_cell_expansion line 45

Source documentation

The kernels may depend on the entire residue-cell assignment. Summing their atomic integrals is exactly the original normalized prime expectation of the appropriate kernel at each prime tuple.

theorem original_prime_cell_expansion {J C : Type*} [Fintype J] [Fintype C]
    (P : Finset ℕ) (q : J → ℕ) (a : J → C → ℕ) (u v : J → C → ℝ) (c₀ : C)
    (hP : ∀ j, primeCellSupport (q j) (a j) (u j) (v j) ⊆ P)
    (hsep : ∀ j c d, c ≠ d →
      ¬Nat.ModEq (q j) (a j c) (a j d) ∨ v j c ≤ u j d ∨ v j d ≤ u j c)
    (f : (J → C) → BulkIntegrand J) :
    let S := fun j => primeCellSupport (q j) (a j) (u j) (v j)
…

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