OAI/NumberTheory/Ostmann/Construction/OriginalAveragedTransfer.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.reconstructedOffDiagonal line 12
2. theorem OAI.Ostmann.original_averaged_pivot_transfer line 21

   Source documentation

   The original prime-tuple prior, both Cauchy steps, and the entire integer off-diagonal are included in this normalized transfer inequality.

   theorem original_averaged_pivot_transfer {A Y : Type*} [Fintype A] [Fintype Y]
       (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)
       (μ : Y → ℝ) (hμ : ∀ y, 0 ≤ μ y) (hmass : ∑ y, μ y ≤ 1)
       (row : Y → (x : Fin n → P) → Fin (∏ i, (x i : ℕ)) → ℂ)
       (hrow : ∀ y x, x ∈ S → ∀ u, ‖row y x u‖ ≤ 1)
       (L : A → ℕ) (v : A → ℤ) (c : Y → ℕ → A → ℂ)
       (hcoprime : ∀ y M, M ∈ T → ∀ a, c y M a ≠ 0 → (L a).Coprime M)
   …