MovingPatternPriorArithmetic.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Arithmetic support under the unchanged representative prior

theorem OAI.Ostmann.allFrequencyList_subtype_mem line 12
Source documentation
The literal list of frequencies still lies in the finite source set.
```
theorem allFrequencyList_subtype_mem (S : Finset ℤ) (n : ℕ)
    (t : FrequencyTree S n) (s : ℤ)
    (hs : s ∈ allFrequencyList n (frequencyTreeMap Subtype.val n t)) : s ∈ S := by
…
```
Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.allFrequencyList, OAI.Ostmann.frequencyTreeMap

theorem OAI.Ostmann.movingPattern_prior_arithmetic_support line 29

Source documentation

Range separation supplies the arithmetic support used when averaging internal primes. The conclusion holds on the actual product prior, before restricting to a nonzero observable.

theorem movingPattern_prior_arithmetic_support {A B C I : Type*} {N n m : ℕ}
    (e : Fin (N + 1) ≃ B ⊕ C) (μ : ℕ → A → ℝ) (ν : B → A → ℝ)
    (prime : A → ℕ) (hinj : Function.Injective prime) (hprime : ∀ a, (prime a).Prime)
    (pattern : Bool × MovingSampleIndex n → C)
    (rep : ∀ c, {i : Bool × MovingSampleIndex n // pattern i = c})
    (tier : A → ℕ) (tierB : B → ℕ) (tierC : C → ℕ)
    (hμtier : ∀ j, j < n → ∀ a, μ j a ≠ 0 → tier a = j)
    (hνtier : ∀ j a, ν j a ≠ 0 → tier a = tierB j) (hB : ∀ b, n ≤ tierB b)
    (htierC : ∀ i, tierC (pattern i) = movingSampleTier i.2)
    (S : Finset ℤ) (V lo : ℕ) (ft : FrequencyTree (S × S) n)
    (hS : ∀ s ∈ S, s ≠ 0 ∧ s.natAbs ≤ V) (hVlo : V ≤ lo)
    (hμlo : ∀ j a, μ j a ≠ 0 → lo < prime a)
…

Mentions: OAI.Ostmann.MovingSampleIndex, OAI.Ostmann.movingSampleTier, OAI.Ostmann.FrequencyTree