OAI/NumberTheory/Ostmann/Construction/AllMultipleTupleWeight.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The harmonic square-root weight of tuples with no singleton

  1. theorem OAI.Ostmann.tuple_range_fiber_card_le line 14
  2. theorem OAI.Ostmann.all_multiple_sqrt_weight line 41
  3. def OAI.Ostmann.allMultipleTuples line 59
  4. theorem OAI.Ostmann.exists_singleton_of_not_allMultiple line 63
  5. theorem OAI.Ostmann.all_multiple_tuple_weight_le line 88

    Source documentation

    Grouping by the distinct value set pays at most n^n for the ordered assignments, while each distinct prime contributes its full harmonic weight.

    theorem all_multiple_tuple_weight_le {A : Type*} [Fintype A] (n : ℕ) (w : A → ℝ)
    (hw0 : ∀ a, 0 ≤ w a) (hw1 : ∀ a, w a ≤ 1) :
    (∑ x ∈ allMultipleTuples A n, ∏ i, Real.sqrt (w (x i))) ≤
      (n : ℝ) ^ n * ∏ a, (1 + w a) := by
…

    Mentions: OAI.Ostmann.allMultipleTuples

  6. theorem OAI.Ostmann.all_multiple_tuple_weight_exp line 120