MovingPatternPrimeBulk.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Exact selected-prime mean of the original pattern kernel

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

theorem OAI.Ostmann.movingPatternPrimeBulkHaar_mean line 56

Source documentation

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

theorem movingPatternPrimeBulkHaar_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