DistinctMomentAverage.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Passing the physical distinct moment to a uniform finite average

theorem OAI.Ostmann.weighted_distinct_average_le line 12

theorem OAI.Ostmann.amplified_distinct_first_mean line 53

Source documentation

The amplified lower bound forces the uniform first moment needed by the finite witness-probability argument.

theorem amplified_distinct_first_mean {ι A : Type*} [Fintype A] [DecidableEq A]
    (w : ι → ℝ) (y : ι → A → ℝ) (hw : ∀ i, 0 ≤ w i)
    (hy : ∀ i a, |y i a| ≤ 1) (hws : Summable w)
    (k : ℕ) (F : (Fin k ↪ A) → ℝ) (X K : ℝ) (hX : 0 < X) (hK : 3000 ≤ K)
    (hF : ∀ e, 0 ≤ F e) (hkA : k ≤ Fintype.card A)
    (hb : ∀ e, |∑' i, w i * ∏ j, y i (e j)| ≤ 2 * Real.sqrt X * F e)
    (hlower : Real.sqrt X * Real.exp ((2 / 125 : ℝ) * K) / 2 ≤
      ∑' i, w i * ternaryDistinctMean (y i) k) :
    Real.exp ((3 / 200 : ℝ) * K) ≤
      (Fintype.card (Fin k ↪ A) : ℝ)⁻¹ * ∑ e, F e := by
…

Mentions: OAI.Ostmann.ternaryDistinctMean