MovingPatternLogPrimeBulk.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Exact selected-prime mean of the original pattern kernel

def OAI.Ostmann.movingPatternLogPrimeBulkHaar line 43
Source documentation
This is the original real kernel and its original Page and spectator averages, evaluated after inserting the selected prime draws.
```
noncomputable def movingPatternLogPrimeBulkHaar (x : (TreeLeafIndex n × Fin m) → primes) : ℂ :=
…
```
Mentions: OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.primes

theorem OAI.Ostmann.movingPatternLogPrimeBulkHaar_mean line 59

Source documentation

Removing the fixed nonbulk primes is sufficient for the supported arithmetic identity. The averaging law and its normalizers remain unchanged.

theorem movingPatternLogPrimeBulkHaar_mean
    [NeZero (∏ i, bulkResidueModuli r p i)]
    (u v : (TreeLeafIndex n × Fin m) → Cell → ℝ)
    (c₀ : Cell × (ZMod (∏ i, bulkResidueModuli r p i))ˣ)
    (S deleted : (TreeLeafIndex n × Fin m) → Finset ℕ)
    (hS : ∀ j, S j ⊆ primeCellSupport (∏ i, bulkResidueModuli r p i)
      (fun c : Cell × (ZMod (∏ i, bulkResidueModuli r p i))ˣ => c.2.val.val)
      (fun c => u j c.1) (fun c => v j c.1))
    (hdeleted : ∀ j i, i ∉ Set.range (movingPatternBulkEmbedding e slot) → base i ∈ deleted j)
    (hout : ∀ q ∈ outside, q.Prime)
    (hdeletedOut : ∀ j q, q ∈ outside → q ∈ deleted j) :
    let M := ∏ i, bulkResidueModuli r p i
…

Mentions: OAI.Ostmann.bulkResidueModuli, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.primeCellSupport, OAI.Ostmann.movingPatternBulkEmbedding