OAI/NumberTheory/Ostmann/Arithmetic/MovingPrimeDominatedLineComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.moving_prime_dominated_line_product_comparison line 14

   Source documentation

   The complete original pattern weight may be used directly once its product of line scalars is dominated by the representative priors. In particular, the pattern law is not assumed to be independent.

   theorem moving_prime_dominated_line_product_comparison {A J : Type*}
       [Fintype A] [Nonempty A] [Fintype J] {N n : ℕ}
       (prime : A → ℕ) (hpInj : Function.Injective prime) (hprime : ∀ a, (prime a).Prime)
       (T : Bool → MovingSlotData (Fin (N + 1)) n) (tier : Fin (N + 1) → ℕ)
       (hlevels : ∀ side, (T side).Levels tier)
       (rep : J → Fin (N + 1)) (base : ∀ j, MovingPairRepresentativeOccurrences T (rep j))
       (d : ℕ) (F U : ℝ) (hF : 1 ≤ F) (hU : 1 ≤ U)
       (hsize : ∀ side, (T side).SizeLE d)
       (hfreq : ∀ side, (T side).Frequencies (fun s => |(s : ℝ)| ≤ F))
       (hvalues : ∀ a, |((prime a : ℤ) : ℝ)| ≤ U)
       (μ : Fin (N + 1) → A → ℝ) (hμ : ∀ i a, 0 ≤ μ i a)
       (hmass : ∀ i, ∑ a, μ i a = 1)
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.MovingPairRepresentativeOccurrences