HarmonicRepeatedMass.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Repeated tuples under the original normalized harmonic priors

theorem OAI.Ostmann.weighted_all_multiple_mass_le line 12
theorem OAI.Ostmann.harmonic_all_multiple_mass_le line 50
theorem OAI.Ostmann.harmonic_all_multiple_integral_bound line 70
theorem OAI.Ostmann.inverse_sqrt_exp_product line 91

theorem OAI.Ostmann.harmonic_repeated_gap_bound line 102

Source documentation

The exact square-root scale of the all-multiple error, before choosing the large gap constant. The harmonic normalizers are retained explicitly.

theorem harmonic_repeated_gap_bound (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
    (n : ℕ) (Q : Fin n → Finset ℕ) (E : Finset (Fin n → P))
    (hE : E ⊆ allMultipleTuples P n) (X D C : ℝ) (hX : 0 < X) (hC : 0 ≤ C)
    (hprod : ∀ x ∈ E, X * Real.exp D ≤ ∏ i, (x i : ℝ))
    (F : (Fin n → P) → ℂ) (hF : ∀ x ∈ E, ‖F x‖ ≤ X * C) :
    ‖∑ x ∈ E, (productPrior (fun i => primeSubsetPrior P (Q i)) x : ℂ) * F x‖ ≤
      Real.sqrt X * (C * (∏ i, (∑ p ∈ Q i, (p : ℝ)⁻¹)⁻¹) * (n : ℝ) ^ n *
        Real.exp ((∑ p : P, (p : ℝ)⁻¹) - D / 2)) := by
…

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