MovingPatternTwoPrimeBulk.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Exact selected-prime mean of the original pattern kernel

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

theorem OAI.Ostmann.movingPatternTwoPrimeBulkHaar_mean line 57

Source documentation

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

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