OAI/NumberTheory/Ostmann/Arithmetic/PrimeLineScalar.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.internalLineScalar_prime_le_twice line 10
2. theorem OAI.Ostmann.prime_line_scalar_product_le line 25
3. theorem OAI.Ostmann.movingPattern_fin_prime_prior_bound line 37

   Source documentation

   The change of giant law costs two per internal equality class, never per external or bulk coordinate.

   theorem movingPattern_fin_prime_prior_bound {A B C : Type*}
       [Fintype B] [Fintype C] {N : ℕ}
       (e : Fin (N + 1) ≃ B ⊕ C) (μ : ℕ → A → ℝ) (ν : B → A → ℝ) (prime : A → ℕ)
       (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)
       (hbound : ∀ j a, (prime a : ℝ) * μ j a ≤ E)
       (G : (Fin (N + 1) → A) → ℂ) (D : ℝ) (hD : 0 ≤ D) (hG : ∀ x, ‖G x‖ ≤ D)
       (x : Fin (N + 1) → A) :
       let W := ((∏ b, ν b (x (e.symm (.inl b))) : ℝ) : ℂ) *
   …

   Mentions: OAI.Ostmann.MovingSampleIndex