Weighted dyadic sum bounds

Real-power identities, shell estimates, and cofinal finite-sum bounds shared by simple-zero and multiplicity-weighted Hadamard growth estimates.

theorem Hadamard.DyadicBounds.dyadic_power_quotient (Ccount lam δ : ℝ) (p k : ℕ) : Ccount * (2 ^ (k + 1)) ^ (lam + δ) * (1 / (2 ^ k) ^ p) = 2 ^ (lam + δ) * Ccount * (2 ^ (lam + δ - ↑p)) ^ k

Rewrite a dyadic growth bound divided by a natural power as a geometric term.

theorem Hadamard.DyadicBounds.geometric_sum_from_le (q : ℝ) (hq_pos : 0 < q) (hq_lt_one : q < 1) (n t : ℕ) : ∑ i ∈ Finset.range t, q ^ (n + 1 + i) ≤ q ^ (n + 1) * (1 - q)⁻¹

Bound a finite geometric tail by the corresponding infinite tail.

theorem Hadamard.DyadicBounds.dyadic_shell_sum_bound {ι : Type u_1} [DecidableEq ι] (z : ι → ℂ) (w : ι → ℝ) (hw : ∀ (ρ : ι), 0 ≤ w ρ) (ball : ℕ → Finset ι) (hmem : ∀ (k : ℕ) (ρ : ι), ρ ∈ ball k ↔ ‖z ρ‖ ≤ 2 ^ k) (p n k : ℕ) (hk : n + 1 ≤ k) (Ccount lam δ : ℝ) (hcount : ∑ ρ ∈ ball (k + 1), w ρ ≤ Ccount * (2 ^ (k + 1)) ^ (lam + δ)) : (∑ ρ ∈ ball (k + 1) \ ball k, if 2 ^ (n + 1) < ‖z ρ‖ then w ρ / ‖z ρ‖ ^ (p + 1) else 0) ≤ 2 ^ (lam + δ) * Ccount * (2 ^ (lam + δ - (↑p + 1))) ^ k

Bound a weighted dyadic shell using the weight of its enclosing ball.

theorem Hadamard.DyadicBounds.tsum_le_of_cofinal_finset_bound {ι : Type u_1} (ball : ℕ → Finset ι) (g : ι → ℝ) {B : ℝ} (hB : 0 ≤ B) (hg : ∀ (i : ι), 0 ≤ g i) (hcofinal : ∀ (t : Finset ι), ∃ (n : ℕ), t ⊆ ball n) (hball : ∀ (n : ℕ), ∑ i ∈ ball n, g i ≤ B) : ∑' (i : ι), g i ≤ B

A uniform bound on sums over cofinal finite sets bounds the infinite sum.

theorem Hadamard.DyadicBounds.cutoff_finsum_eq_sum {ι : Type u_1} (s : Finset ι) (P : ι → Prop) [DecidablePred P] (f : ι → ℝ) (hs : ∀ (a : ι), a ∈ s ↔ P a) : (∑ᶠ (a : ι), if P a then f a else 0) = ∑ a ∈ s, f a

A cutoff supported on a finite set has the corresponding finite sum.

theorem Hadamard.DyadicBounds.sum_le_of_geometric_shells {ι : Type u_1} [DecidableEq ι] (ball : ℕ → Finset ι) (g : ι → ℝ) (A q : ℝ) (hA : 0 ≤ A) (hq_pos : 0 < q) (hq_lt : q < 1) (n m : ℕ) (hsub : ∀ (k : ℕ), ball k ⊆ ball (k + 1)) (hzero : ∀ k ≤ n + 1, ∑ i ∈ ball k, g i = 0) (hshell : ∀ (k : ℕ), n + 1 ≤ k → ∑ i ∈ ball (k + 1) \ ball k, g i ≤ A * q ^ k) : ∑ i ∈ ball m, g i ≤ A * q / (1 - q) * q ^ n

A nested sequence of finite sets with geometrically bounded shells has a bounded tail.

theorem Hadamard.DyadicBounds.dyadic_ball_cofinal {ι : Type u_1} (z : ι → ℂ) (ball : ℕ → Finset ι) (hmem : ∀ (k : ℕ) (ρ : ι), ρ ∈ ball k ↔ ‖z ρ‖ ≤ 2 ^ k) (t : Finset ι) : ∃ (m : ℕ), t ⊆ ball m

Every finite set lies in one member of a dyadic ball exhaustion.