OAI/NumberTheory/Ostmann/Arithmetic/MovingHarmonicKeyMass.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.indexed_harmonic_key_mass line 12

   Source documentation

   On a fixed giant and frequency, the regular tuple determines the row. Zero rows are discarded exactly; the other rows retain their original mass.

   theorem indexed_harmonic_key_mass {A I : Type*} [Fintype A] [Fintype I]
       (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) (Q : I → Finset ℕ)
       (X : A → ℕ) (y : A → I → P) (v : A → ℤ) (μ : A → ℝ)
       (g : ℕ → ℝ) (hg : ∀ q, 0 ≤ g q)
       (hrow : ∀ a b, X a = X b → y a = y b → v a = v b → a = b)
       (hinj : ∀ a, μ a ≠ 0 → Function.Injective (y a))
       (hpoint : ∀ a, μ a ≠ 0 →
         μ a ≤ g (X a) * ∏ i, primeSubsetPrior P (Q i) (y a i))
       (k : ℕ × ℕ × ℤ) :
       (∑ a, if (X a, (∏ i, (y a i : ℕ)), v a) = k then μ a else 0) ≤
         g k.1 * ((Fintype.card I).factorial : ℝ) *
           (∏ i, (∑ p ∈ Q i, (p : ℝ)⁻¹)⁻¹) * (k.2.1 : ℝ)⁻¹ := by
   …

   Mentions: OAI.Ostmann.primeSubsetPrior