OAI/NumberTheory/Ostmann/Construction/OriginalDirectedTransfer.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.groupedDirectedAmplitude line 12
2. theorem OAI.Ostmann.original_directed_transfer line 33

   Source documentation

   This is the normalized transfer inequality with its actual prime residue row and its next copied directed amplitude, rather than an assumed recurrence.

   theorem original_directed_transfer {A H Y Z : Type*}
       [Fintype A] [Fintype H] [Fintype Y] [Fintype Z]
       (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 ℕ) (hT : ∀ M ∈ T, 0 < M) (hST : ∀ x ∈ S, (∏ i, (x i : ℕ)) ∈ T)
       (χP : Fin n → ∀ p : ℕ, DirichletCharacter ℂ p)
       (κ : Fin n → P → ℂ) (hκ : ∀ i p, ‖κ i p‖ ≤ 1) (ε : Fin n → ℤ)
       (L : A → H → ℕ) (U : Z → Y → ℕ)
       [∀ a h, Fact (L a h).Prime] [∀ z y, Fact (U z y).Prime]
       (t : ∀ p : ℕ, ZMod p)
   …