MovingPatternLogPrimeObservable.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The literal prime observable in the original nonbulk Fubini formula

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

theorem OAI.Ostmann.movingPatternLogPrimeObservable_eq line 46

Source documentation

The terminal log factors are real weights, depending only on the regular prime assignment and not on either giant variable.

theorem movingPatternLogPrimeObservable_eq (x : Fin (N + 1) → primes) :
    movingPatternLogPrimeObservable 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 logSlots cb x =
    ((∏ j, bulkLogCutoffWeight (fun i => ((x i : ℕ) : ℝ)) cb (logSlots j) : ℝ) : ℂ) *
      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 x := rfl

Mentions: OAI.Ostmann.primes, OAI.Ostmann.movingPatternLogPrimeObservable, OAI.Ostmann.bulkLogCutoffWeight, OAI.Ostmann.movingPatternPrimeObservable

theorem OAI.Ostmann.movingPatternLogPrimeObservable_join line 55

theorem OAI.Ostmann.movingPatternBulkMean_logPrimeObservable line 96

Source documentation

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

theorem movingPatternBulkMean_logPrimeObservable (base : Fin (N + 1) → primes)
    (ν : B → primes → ℝ) (initial : (TreeLeafIndex n × Fin m) → Finset ℕ)
    (hν : ∀ j, ν (slot j) = primeSubsetPrior primes (initial j)) :
    movingPatternBulkMean e ν slot
      (movingPatternLogPrimeObservable 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 logSlots cb) base =
    ∑ z : TreeLeafIndex n × Fin m → primes,
      ((∏ j, primeSubsetPrior primes (initial j) (z j) : ℝ) : ℂ) *
        movingPatternLogPrimeBulkHaar 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 logSlots cb z := by
…

Mentions: OAI.Ostmann.primes, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.primeSubsetPrior, OAI.Ostmann.movingPatternBulkMean, OAI.Ostmann.movingPatternLogPrimeObservable, OAI.Ostmann.movingPatternLogPrimeBulkHaar