MovingPatternBulkMajorant.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Integrating nonuniform errors under the original pattern law

theorem OAI.Ostmann.movingPattern_flagged_pointwise_bound line 10

theorem OAI.Ostmann.movingPattern_signed_bulk_majorant line 31

Source documentation

A variable bound for the literal signed bulk mean is integrated against the original external and representative priors. In particular the large pointwise spectator error is averaged, rather than replaced by its supremum.

theorem movingPattern_signed_bulk_majorant {A B C : Type*}
    [Fintype A] [Fintype B] [Fintype C] {N n m : ℕ}
    (e : Fin (N + 1) ≃ B ⊕ C) (μ : ℕ → A → ℝ) (ν : B → A → ℝ) (prime : A → ℕ)
    (t : Bool → FrequencyTree ℤ n) (small : Bool → TreeLeafTuple (List B) n)
    (slot : (TreeLeafIndex n × Fin m) ↪ B) (perm : Equiv.Perm (TreeLeafIndex n × Fin m))
    (pattern : Bool × MovingSampleIndex n → C)
    (rep : ∀ c, {i : Bool × MovingSampleIndex n // pattern i = c}) (E : ℝ) (hE : 0 ≤ E)
    (hprime : ∀ a, (prime a).Prime) (hμ : ∀ j a, 0 ≤ μ j a) (hν : ∀ j a, 0 ≤ ν j a)
    (hnmass : ∀ j, ∑ a, ν j a = 1)
    (hbound : ∀ j a, (prime a : ℝ) * μ j a ≤ E)
    (G : (Fin (N + 1) → A) → ℂ) (D : (Fin (N + 1) → A) → ℝ)
    (hG : ∀ x, ‖movingPatternBulkMean e ν slot G x‖ ≤ D x)
…

Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.MovingSampleIndex, OAI.Ostmann.movingPatternBulkMean