MovingPatternTwoPrimeObservable.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The literal prime observable in the original nonbulk Fubini formula

def OAI.Ostmann.movingPatternTwoPrimeObservable 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 movingPatternTwoPrimeObservable (x : Fin (N + 1) → primes) : ℂ :=
…
```
Mentions: OAI.Ostmann.primes
theorem OAI.Ostmann.movingPatternTwoPrimeObservable_join line 41

theorem OAI.Ostmann.movingPatternBulkMean_twoPrimeObservable line 81

Source documentation

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

theorem movingPatternBulkMean_twoPrimeObservable (base : Fin (N + 1) → primes)
    (ν : B → primes → ℝ) (initial : (TreeLeafIndex n × Fin m) → Finset ℕ)
    (hν : ∀ j, ν (slot j) = primeSubsetPrior primes (initial j)) :
    movingPatternBulkMean e ν slot
      (movingPatternTwoPrimeObservable e t small slot perm pattern primes hprimes
        childBound pivotBound hfreq F E outside R r p g twist P Q xg y ψ X lo hi hlo hhi φ G L U) base =
    ∑ z : TreeLeafIndex n × Fin m → primes,
      ((∏ j, primeSubsetPrior primes (initial j) (z j) : ℝ) : ℂ) *
        movingPatternTwoPrimeBulkHaar 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 xg 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.movingPatternTwoPrimeObservable, OAI.Ostmann.movingPatternTwoPrimeBulkHaar