MovingPatternPriorRanges.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Actual prior support supplies the level and prime-separation hypotheses

theorem OAI.Ostmann.movingPattern_internal_prior_nonzero line 11

theorem OAI.Ostmann.movingPattern_tier_consistent_of_nonzero line 33

Source documentation

Incompatible level identifications have zero original weight. This permits retaining all setoids in the exact expansion.

theorem movingPattern_tier_consistent_of_nonzero {A B C : Type*} [Fintype B] {N n : ℕ}
    (e : Fin (N + 1) ≃ B ⊕ C) (μ : ℕ → A → ℝ) (ν : B → A → ℝ)
    (prime : A → ℕ) (pattern : Bool × MovingSampleIndex n → C)
    (rep : ∀ c, {i : Bool × MovingSampleIndex n // pattern i = c})
    (tier : A → ℕ) (hμ : ∀ j, j < n → ∀ a, μ j a ≠ 0 → tier a = j)
    (G : (Fin (N + 1) → A) → ℂ) (x : Fin (N + 1) → A)
    (hx : movingOriginalPatternWeight e μ ν prime n pattern G x ≠ 0) :
    ∀ i, movingSampleTier (rep (pattern i)).val.2 = movingSampleTier i.2 := by
…

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

theorem OAI.Ostmann.movingPattern_zero_of_inconsistent_tiers line 48
theorem OAI.Ostmann.movingPattern_prior_tiers line 59
theorem OAI.Ostmann.movingPattern_prior_prime_separation line 76