MovingPatternPrimeObservable.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The literal prime observable in the original nonbulk Fubini formula

def OAI.Ostmann.movingPatternPrimeObservable line 30
Source documentation
The coefficient before selecting or conditioning any of its bulk coordinates. All original frequency and coprimality gates are retained.
```
noncomputable def movingPatternPrimeObservable (x : Fin (N + 1) → primes) : ℂ :=
…
```
Mentions: OAI.Ostmann.primes
theorem OAI.Ostmann.movingPatternPrimeObservable_join line 41

theorem OAI.Ostmann.movingPatternBulkMean_primeObservable line 81

Source documentation

This is exactly the selected-coordinate average used by the signed pattern majorant, under the initial word law.

theorem movingPatternBulkMean_primeObservable (base : Fin (N + 1) → primes)
    (ν : B → primes → ℝ) (initial : (TreeLeafIndex n × Fin m) → Finset ℕ)
    (hν : ∀ j, ν (slot j) = primeSubsetPrior primes (initial j)) :
    movingPatternBulkMean e ν slot
      (movingPatternPrimeObservable e t small slot perm pattern primes hprimes
        childBound pivotBound hfreq F E outside R r p g twist P Q y ψ X lo hi hlo hhi φ G L U) base =
    ∑ z : TreeLeafIndex n × Fin m → primes,
      ((∏ j, primeSubsetPrior primes (initial j) (z j) : ℝ) : ℂ) *
        movingPatternPrimeBulkHaar e t small slot perm pattern (fun i => (base i : ℕ)) primes
          hprimes (fun i _ => hprimes _ (base i).property) childBound pivotBound hfreq F E outside
          R r p g twist P Q y ψ X lo hi hlo hhi φ G L U z := by
…

Mentions: OAI.Ostmann.primes, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.primeSubsetPrior, OAI.Ostmann.movingPatternBulkMean, OAI.Ostmann.movingPatternPrimeObservable, OAI.Ostmann.movingPatternPrimeBulkHaar