OAI/NumberTheory/Ostmann/Arithmetic/MovingPrimePatternFlagBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingPrimePattern_flagged_weight_bound line 11
2. theorem OAI.Ostmann.movingPrimePattern_flagged_mean_bound line 43

   Source documentation

   After normalization, all the symbolic internal factors cost only the number of internal draws. There is no factor counting the external slots.

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

   Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSampleIndex, OAI.Ostmann.movingOriginalPatternWeight, OAI.Ostmann.movingPatternPrimeFlagProduct