OAI/NumberTheory/Ostmann/Construction/OriginalPivotTransfer.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.positiveIntegerPivotKey line 11
2. theorem OAI.Ostmann.transferPrimeTupleProduct_pos line 15
3. def OAI.Ostmann.primeTuplePivotKey line 19
4. theorem OAI.Ostmann.original_pivot_transfer_real line 25

   Source documentation

   All coprimality and interval restrictions may remain in c. The extended integer has no prime tuple or character attached to it.

   theorem original_pivot_transfer_real {A : Type*} [Fintype A]
       (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
       {n : ℕ} (Q : Fin n → Finset ℕ) (hQP : ∀ i, Q i ⊆ P)
       (hQ : ∀ i, (∑ p ∈ Q i, (p : ℝ)⁻¹) ≠ 0)
       (S : Finset (Fin n → P)) (hS : ∀ x ∈ S, Function.Injective x)
       (T : Finset ℕ) (hTpos : ∀ M ∈ T, 0 < M)
       (hT : ∀ x ∈ S, (∏ i, (x i : ℕ)) ∈ T)
       (row : ∀ x : Fin n → P, Fin (∏ i, (x i : ℕ)) → ℂ)
       (hrow : ∀ x ∈ S, ∀ u, ‖row x u‖ ≤ 1)
       (L : A → ℕ) (v : A → ℤ) (c : ℕ → A → ℂ)
       (hL : ∀ M ∈ T, ∀ a, c M a ≠ 0 → (L a).Coprime M) :
       ‖∑ x ∈ S, (productPrior (fun i => primeSubsetPrior P (Q i)) x : ℂ) *
   …

   Mentions: OAI.Ostmann.productPrior, OAI.Ostmann.primeSubsetPrior