OAI/NumberTheory/Ostmann/Arithmetic/MovingHarmonicProductFiber.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.card_indexed_distinct_prime_product_fiber line 11
2. theorem OAI.Ostmann.indexed_harmonic_product_point_bound line 46
3. theorem OAI.Ostmann.indexed_harmonic_distinct_product_mass line 64

   Source documentation

   Reindexing the regular roles changes neither the original harmonic normalizers nor the factorial cost of a distinct-prime product fibre.

   theorem indexed_harmonic_distinct_product_mass {I : Type*} [Fintype I]
       (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) (Q : I → Finset ℕ)
       (S : Finset (I → P)) (hS : ∀ x ∈ S, Function.Injective x) (M : ℕ) :
       (∑ x ∈ S.filter (fun x : I → P => (∏ i, (x i : ℕ)) = M),
         (∏ i, primeSubsetPrior P (Q i) (x i))) ≤
         ((Fintype.card I).factorial : ℝ) *
           (∏ i, (∑ p ∈ Q i, (p : ℝ)⁻¹)⁻¹) * (M : ℝ)⁻¹ := by
   …

   Mentions: OAI.Ostmann.primeSubsetPrior