MovingPatternLogTwoPrimeBulk.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Exact selected-prime mean of the original pattern kernel

def OAI.Ostmann.movingPatternLogTwoPrimeBulkHaar 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 movingPatternLogTwoPrimeBulkHaar (x : (TreeLeafIndex n × Fin m) → primes) : ℂ :=
…
```
Mentions: OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.primes

theorem OAI.Ostmann.movingPatternLogTwoPrimeBulkHaar_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 movingPatternLogTwoPrimeBulkHaar_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