OAI/NumberTheory/Ostmann/Construction/PrimeTupleDiagonal.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.distinctTuplePrior line 11
2. theorem OAI.Ostmann.distinctTuplePrior_nonneg line 15
3. theorem OAI.Ostmann.distinctTuplePrior_key_mass line 25

   Source documentation

   This is the quantitative counterpart mass for the exact diagonal key. The distinctness mask discards tuples, without renormalizing any marginal.

   theorem distinctTuplePrior_key_mass {n : ℕ} (P : Finset ℕ)
       (hP : ∀ p ∈ P, p.Prime) (μ : Fin n → P → ℝ) (C : Fin n → ℝ)
       (hμ : ∀ i p, 0 ≤ μ i p) (hC : ∀ i, 0 ≤ C i)
       (hbound : ∀ i (p : P), (p : ℝ) * μ i p ≤ C i) (V : ℕ) (k : ℕ × ℤ) :
       (∑ a : (Fin n → P) × transferFrequencyRange V,
         if ((∏ i, (a.1 i : ℕ)), (a.2 : ℤ)) = k then distinctTuplePrior P μ a.1 else 0) ≤
         (n.factorial : ℝ) * (∏ i, C i) * (k.1 : ℝ)⁻¹ := by
   …

   Mentions: OAI.Ostmann.transferFrequencyRange, OAI.Ostmann.distinctTuplePrior

4. theorem OAI.Ostmann.prime_tuple_pivot_diagonal_bound line 48

   Source documentation

   The Section 7 diagonal with the actual regular Fourier multiplier. It pays a single factorial counterpart cost and keeps the exact one-sided energy, rather than taking absolute values of the ungrouped pair terms.

   theorem prime_tuple_pivot_diagonal_bound {n : ℕ}
       (P : Finset ℕ) [∀ p : P, NeZero (p : ℕ)] (hP : ∀ p ∈ P, p.Prime)
       (μ : Fin n → P → ℝ) (C : Fin n → ℝ)
       (hμ : ∀ i p, 0 ≤ μ i p) (hC : ∀ i, 0 ≤ C i)
       (hbound : ∀ i (p : P), (p : ℝ) * μ i p ≤ C i)
       (V M : ℕ) (hlarge : ∀ p : P, V < (p : ℕ))
       (g : ∀ q : ℕ, ZMod q → ℂ)
       (W : ((Fin n → P) × transferFrequencyRange V) → ℂ)
       (hzero : ∀ x, W (x, ⟨0, by simp [transferFrequencyRange]⟩) = 0) :
       (pivotDiagonal (fun a : (Fin n → P) × transferFrequencyRange V => ∏ i, (a.1 i : ℕ))
         (fun a => (a.2 : ℤ))
         (fun a => (distinctTuplePrior P μ a.1 : ℂ) * W a *
   …

   Mentions: OAI.Ostmann.transferFrequencyRange, OAI.Ostmann.pivotDiagonal, OAI.Ostmann.distinctTuplePrior