Geometric decay from product majorants

Let r : ι → ℝ be a nonnegative family, and let x be a real number bounded by every nonnegative bound for the products ∏ i ∈ s, r i over the n-element finite sets s. Such numbers arise as norms of the coefficients of Fredholm determinants and resolvents, which are controlled by products of row bounds. This file turns that hypothesis into tail estimates.

Main results

• TauCeti.exists_geometric_bound_of_tendsto_cofinite: after rescaling by any ρ ≥ 0, a null family is bounded by some B ≥ 1, and by any prescribed q ∈ (0, 1) off a finite set T.
• TauCeti.mul_pow_le_of_forall_prod_le: if ρ * r i ≤ q ≤ 1 off a finite set T and ρ * r i ≤ B everywhere, then x * ρ ^ n ≤ B ^ #T * q ^ (n - #T).
• TauCeti.tendsto_mul_pow_of_forall_prod_le: if r tends to zero along the cofinite filter, then x n * |ρ| ^ n tends to zero for every real ρ.

References

• J.-P. Serre, Endomorphismes complètement continus des espaces de Banach p-adiques, Publ. Math. IHÉS 12 (1962), 69–85, §§4–5.

theorem TauCeti.exists_geometric_bound_of_tendsto_cofinite {ι : Type u_1} {r : ι → ℝ} (hr : Filter.Tendsto r Filter.cofinite (nhds 0)) {ρ q : ℝ} (hρ : 0 ≤ ρ) (hq₀ : 0 < q) (hq₁ : q < 1) : ∃ (T : Finset ι) (B : ℝ), 1 ≤ B ∧ (∀ i ∉ T, ρ * r i ≤ q) ∧ (∀ (i : ι), ρ * r i ≤ B) ∧ Filter.Tendsto (fun (n : ℕ) => B ^ T.card * q ^ (n - T.card)) Filter.atTop (nhds 0)

A null family admits a uniform bound and a finite exceptional set outside which its rescaling is at most any prescribed q ∈ (0, 1). The associated geometric tail tends to zero.

theorem TauCeti.mul_pow_le_of_forall_prod_le {ι : Type u_1} {r : ι → ℝ} (hr : ∀ (i : ι), 0 ≤ r i) {n : ℕ} {x : ℝ} (hx : ∀ (c : ℝ), 0 ≤ c → (∀ (s : Finset ι), s.card = n → ∏ i ∈ s, r i ≤ c) → x ≤ c) {ρ q B : ℝ} (hρ : 0 < ρ) (hq₀ : 0 ≤ q) (hq₁ : q ≤ 1) (hB : 1 ≤ B) (T : Finset ι) (hT : ∀ i ∉ T, ρ * r i ≤ q) (hrB : ∀ (i : ι), ρ * r i ≤ B) : x * ρ ^ n ≤ B ^ T.card * q ^ (n - T.card)

Tail bound from product majorants. Let r be nonnegative, and let x be bounded by every nonnegative bound for the products ∏ i ∈ s, r i over the n-element sets s. If ρ > 0, 0 ≤ q ≤ 1, 1 ≤ B, and T is a finite set of indices with ρ * r i ≤ q off T and ρ * r i ≤ B everywhere, then x * ρ ^ n ≤ B ^ #T * q ^ (n - #T), with truncated subtraction in the exponent. This is the estimate behind the entirety of Fredholm determinants and resolvents.

theorem TauCeti.tendsto_mul_pow_of_forall_prod_le {ι : Type u_1} {r : ι → ℝ} (hr₀ : ∀ (i : ι), 0 ≤ r i) (hr : Filter.Tendsto r Filter.cofinite (nhds 0)) {x : ℕ → ℝ} (hx₀ : ∀ (n : ℕ), 0 ≤ x n) (hx : ∀ (n : ℕ) (c : ℝ), 0 ≤ c → (∀ (s : Finset ι), s.card = n → ∏ i ∈ s, r i ≤ c) → x n ≤ c) (ρ : ℝ) : Filter.Tendsto (fun (n : ℕ) => x n * |ρ| ^ n) Filter.atTop (nhds 0)

Geometric decay from null product majorants. Let r be nonnegative and tend to zero along the cofinite filter, and let x n ≥ 0 be bounded by every nonnegative bound for the products ∏ i ∈ s, r i over the n-element sets s. Then x n * |ρ| ^ n tends to zero for every real ρ.