MovingHarmonicSupport.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Concrete support conditions for the original harmonic role priors

theorem OAI.Ostmann.harmonic_product_mem line 11
theorem OAI.Ostmann.harmonic_product_distinct_levels line 19

theorem OAI.Ostmann.harmonic_product_external_internal line 31

Source documentation

The original internal samples lie strictly below the external tier. Thus the same disjoint shell choice supplies the cross-coordinate condition.

theorem harmonic_product_external_internal {B C : Type*} {N n : ℕ}
    (e : Fin (N + 1) ≃ B ⊕ C) (tierB : B → ℕ) (tierC : C → ℕ)
    (pattern : Bool × MovingSampleIndex n → C)
    (rep : ∀ c, {i : Bool × MovingSampleIndex n // pattern i = c})
    (hB : ∀ b, n ≤ tierB b)
    (htier : ∀ i, tierC (pattern i) = movingSampleTier i.2)
    (P : Finset ℕ) (Q : Fin (N + 1) → Finset ℕ)
    (hQ : ∀ i j, (Sum.elim tierB tierC) (e i) ≠ (Sum.elim tierB tierC) (e j) →
      Disjoint (Q i) (Q j)) (x : Fin (N + 1) → P)
    (hx : productPrior (fun i => primeSubsetPrior P (Q i)) x ≠ 0) :
    ∀ b c, (x (e.symm (.inl b)) : ℕ) ≠ (x (e.symm (.inr c)) : ℕ) := by
…

Mentions: OAI.Ostmann.MovingSampleIndex, OAI.Ostmann.movingSampleTier, OAI.Ostmann.productPrior, OAI.Ostmann.primeSubsetPrior

theorem OAI.Ostmann.intCast_ne_zero_of_natAbs_lt line 54
Source documentation
A nonzero original frequency smaller than an internal prime remains nonzero modulo that prime.
```
theorem intCast_ne_zero_of_natAbs_lt (q : ℕ) (s : ℤ) (hs : s ≠ 0)
    (hqs : s.natAbs < q) : (s : ZMod q) ≠ 0 := by
…
```
theorem OAI.Ostmann.harmonic_product_frequency_units line 62