MovingPrimePatternBulkMajorant.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Integrating nonuniform errors under the original pattern law

theorem OAI.Ostmann.movingPrimePattern_flagged_pointwise_bound line 10

theorem OAI.Ostmann.movingPrimePattern_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 movingPrimePattern_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