OAI/NumberTheory/Ostmann/Construction/WeightedRepeatRemoval.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.weighted_power_approximation line 16

   Source documentation

   A pointwise square-root shift controls the error in the weighted moment. All quantities on the right are the actual unperturbed moments.

   theorem weighted_power_approximation {ι : Type*} (w f D : ι → ℝ)
       (hw : ∀ i, 0 ≤ w i) (hf : ∀ i, 0 ≤ f i) (b : ℝ) (hb : 0 ≤ b)
       (k : ℕ) (hk : 0 < k) (hws : Summable w)
       (hfs : Summable (fun i => w i * f i ^ k))
       (hD : ∀ i, |D i - f i ^ k| ≤ (f i + b) ^ k - f i ^ k) :
       Summable (fun i => w i * D i) ∧
         |(∑' i, w i * D i) - (∑' i, w i * f i ^ k)| ≤
           ((∑' i, w i * f i ^ k) ^ (1 / (k : ℝ)) +
             b * (∑' i, w i) ^ (1 / (k : ℝ))) ^ k - (∑' i, w i * f i ^ k) := by
   …

2. def OAI.Ostmann.ternaryMean line 46
3. def OAI.Ostmann.ternaryDistinctMean line 49
4. theorem OAI.Ostmann.ternaryMean_abs_le_one line 52
5. theorem OAI.Ostmann.weighted_ternary_distinct_moment line 68

   Source documentation

   Actual distinct-index averaging, with no assumed repeat-removal estimate.

   theorem weighted_ternary_distinct_moment {ι A : Type*} [Fintype A] [DecidableEq A]
       (w : ι → ℝ) (y : ι → A → ℝ) (hw : ∀ i, 0 ≤ w i)
       (hy : ∀ i a, y i a = 0 ∨ y i a = 1 ∨ y i a = -1)
       (k : ℕ) (hk : 0 < k) (heven : Even k) (hkA : k ≤ Fintype.card A)
       (hws : Summable w) :
       Summable (fun i => w i * ternaryDistinctMean (y i) k) ∧
         |(∑' i, w i * ternaryDistinctMean (y i) k) -
             (∑' i, w i * ternaryMean (y i) ^ k)| ≤
           ((∑' i, w i * ternaryMean (y i) ^ k) ^ (1 / (k : ℝ)) +
             (Real.sqrt ((k : ℝ) * Fintype.card A) / Fintype.card A) *
               (∑' i, w i) ^ (1 / (k : ℝ))) ^ k -
             (∑' i, w i * ternaryMean (y i) ^ k) := by
   …

   Mentions: OAI.Ostmann.ternaryDistinctMean, OAI.Ostmann.ternaryMean