DyadicSum.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.sum_dyadic_shells line 10

Source documentation

Decompose a positive integer initial interval into dyadic shells.

theorem sum_dyadic_shells {E : Type*} [AddCommMonoid E] (f : ℕ → E) (J : ℕ) :
    (∑ n ∈ Finset.Ico 1 (2 ^ J), f n) =
      ∑ j ∈ Finset.range J, ∑ n ∈ Finset.Ico (2 ^ j) (2 ^ (j + 1)), f n := by
…

theorem OAI.Problem337.norm_sum_dyadic_shells_le line 22

Source documentation

The total cost of dyadic shells is geometric rather than logarithmic.

theorem norm_sum_dyadic_shells_le {E : Type*} [NormedAddCommGroup E]
    (f : ℕ → E) (J : ℕ) (C : ℝ)
    (hlocal : ∀ j < J,
      ‖∑ n ∈ Finset.Ico (2 ^ j) (2 ^ (j + 1)), f n‖ ≤ C * (2 : ℝ) ^ j) :
    ‖∑ n ∈ Finset.Ico 1 (2 ^ J), f n‖ ≤ C * ((2 : ℝ) ^ J - 1) := by
…

theorem OAI.Problem337.norm_sum_interval_le_of_dyadic line 40

Source documentation

Local bounds on the dyadic pieces of any positive integer interval sum with constant at most two; useful for off-diagonal reciprocal phase estimates.

theorem norm_sum_interval_le_of_dyadic {E : Type*} [NormedAddCommGroup E]
    (f : ℕ → E) (Y X : ℕ) (hY : 1 ≤ Y) (C : ℝ) (hC : 0 ≤ C)
    (hlocal : ∀ j : ℕ,
      ‖∑ n ∈ (Finset.Ico (2 ^ j) (2 ^ (j + 1)) ∩ Finset.Icc Y X), f n‖
        ≤ C * (2 : ℝ) ^ j) :
    ‖∑ n ∈ Finset.Icc Y X, f n‖ ≤ 2 * C * X := by
…

theorem OAI.Problem337.norm_sum_interval_le_of_local_intervals line 87

Source documentation

Only dyadic intervals intersecting the target interval need local estimates. Their base points lie between half the lower endpoint and the upper endpoint.

theorem norm_sum_interval_le_of_local_intervals {E : Type*} [NormedAddCommGroup E]
    (f : ℕ → E) (Y X : ℕ) (hY : 1 ≤ Y) (C : ℝ) (hC : 0 ≤ C)
    (hlocal : ∀ U : ℕ, 0 < U → Y ≤ 2 * U → U ≤ X →
      ‖∑ n ∈ (Finset.Ico U (2 * U) ∩ Finset.Icc Y X), f n‖ ≤ C * U) :
    ‖∑ n ∈ Finset.Icc Y X, f n‖ ≤ 2 * C * X := by
…