MovingPatternLogTwoPrimeObservable.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The literal prime observable in the original nonbulk Fubini formula

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

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

Mentions: OAI.Ostmann.primes, OAI.Ostmann.movingPatternLogTwoPrimeObservable, OAI.Ostmann.bulkLogCutoffWeight, OAI.Ostmann.movingPatternTwoPrimeObservable

theorem OAI.Ostmann.movingPatternLogTwoPrimeObservable_join line 55

theorem OAI.Ostmann.movingPatternBulkMean_logTwoPrimeObservable line 96

Source documentation

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

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

Mentions: OAI.Ostmann.primes, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.primeSubsetPrior, OAI.Ostmann.movingPatternBulkMean, OAI.Ostmann.movingPatternLogTwoPrimeObservable, OAI.Ostmann.movingPatternLogTwoPrimeBulkHaar