Coarse-graining support: Support.Book.Ch05.Theorems.Section57.ExponentialKernel

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Exponential kernels for the bad-scale summation

These are pure real-variable summability facts used to sum the fixed-pair probability kernels in the quantitative minimal-scale proof.

noncomputable def HCPolySupport.Book.Ch05.Section57.geometricExpKernelConst (ρ η : ℝ) : ℝ

The sum of the geometric exponential kernel exp (-k * (ρ ^ η - 1)) over natural indices, used in bad-scale probability summation.

Equations

• HCPolySupport.Book.Ch05.Section57.geometricExpKernelConst ρ η = ∑' (k : ℕ), Real.exp (↑k * -(ρ ^ η - 1))

noncomputable def HCPolySupport.Book.Ch05.Section57.linearExpKernelConst (ρ η : ℝ) : ℝ

The sum of the exponential kernel weighted by k + 1, accounting for linear multiplicity in bad-scale probability summation.

Equations

• HCPolySupport.Book.Ch05.Section57.linearExpKernelConst ρ η = ∑' (k : ℕ), (↑k + 1) * Real.exp (↑k * -(ρ ^ η - 1))

theorem HCPolySupport.Book.Ch05.Section57.geometricExpKernelConst_pos {ρ η : ℝ} (hρ : 1 < ρ) (hη : 0 < η) : 0 < geometricExpKernelConst ρ η

theorem HCPolySupport.Book.Ch05.Section57.summable_linear_exp_kernel {ρ η : ℝ} (hρ : 1 < ρ) (hη : 0 < η) : Summable fun (k : ℕ) => (↑k + 1) * Real.exp (↑k * -(ρ ^ η - 1))

theorem HCPolySupport.Book.Ch05.Section57.linearExpKernelConst_pos {ρ η : ℝ} (hρ : 1 < ρ) (hη : 0 < η) : 0 < linearExpKernelConst ρ η

theorem HCPolySupport.Book.Ch05.Section57.exp_neg_rpow_mul_pow_le_exp_neg_mul_exp_neg_nat {A ρ η : ℝ} (hA : 1 ≤ A) (hρ : 1 < ρ) (hη : 0 < η) (k : ℕ) : Real.exp (-(A * ρ ^ k) ^ η) ≤ Real.exp (-A ^ η) * Real.exp (-((ρ ^ η - 1) * ↑k))

theorem HCPolySupport.Book.Ch05.Section57.summable_exp_neg_rpow_mul_pow {A ρ η : ℝ} (hA : 1 ≤ A) (hρ : 1 < ρ) (hη : 0 < η) : Summable fun (k : ℕ) => Real.exp (-(A * ρ ^ k) ^ η)

theorem HCPolySupport.Book.Ch05.Section57.tsum_exp_neg_rpow_mul_pow_le {A ρ η : ℝ} (hA : 1 ≤ A) (hρ : 1 < ρ) (hη : 0 < η) : ∑' (k : ℕ), Real.exp (-(A * ρ ^ k) ^ η) ≤ ∑' (k : ℕ), Real.exp (-A ^ η) * Real.exp (-((ρ ^ η - 1) * ↑k))

theorem HCPolySupport.Book.Ch05.Section57.tsum_exp_neg_rpow_mul_pow_le_const {A ρ η : ℝ} (hA : 1 ≤ A) (hρ : 1 < ρ) (hη : 0 < η) : ∑' (k : ℕ), Real.exp (-(A * ρ ^ k) ^ η) ≤ Real.exp (-A ^ η) * geometricExpKernelConst ρ η

theorem HCPolySupport.Book.Ch05.Section57.tsum_linear_mul_exp_neg_rpow_mul_pow_le_const {A ρ η : ℝ} (hA : 1 ≤ A) (hρ : 1 < ρ) (hη : 0 < η) : ∑' (k : ℕ), (↑k + 1) * Real.exp (-(A * ρ ^ k) ^ η) ≤ Real.exp (-A ^ η) * linearExpKernelConst ρ η

theorem HCPolySupport.Book.Ch05.Section57.summable_linear_mul_exp_neg_rpow_mul_pow {A ρ η : ℝ} (hA : 1 ≤ A) (hρ : 1 < ρ) (hη : 0 < η) : Summable fun (k : ℕ) => (↑k + 1) * Real.exp (-(A * ρ ^ k) ^ η)

theorem HCPolySupport.Book.Ch05.Section57.summable_exp_neg_two_rpow_mul_pow {A ρ₁ ρ₂ η : ℝ} (hA : 1 ≤ A) (hρ₁ : 1 < ρ₁) (hρ₂ : 1 < ρ₂) (hη : 0 < η) : Summable fun (p : ℕ × ℕ) => Real.exp (-(A * ρ₁ ^ p.1 * ρ₂ ^ p.2) ^ η)

theorem HCPolySupport.Book.Ch05.Section57.tsum_exp_neg_two_rpow_mul_pow_le_const {A ρ₁ ρ₂ η : ℝ} (hA : 1 ≤ A) (hρ₁ : 1 < ρ₁) (hρ₂ : 1 < ρ₂) (hη : 0 < η) : ∑' (p : ℕ × ℕ), Real.exp (-(A * ρ₁ ^ p.1 * ρ₂ ^ p.2) ^ η) ≤ Real.exp (-A ^ η) * geometricExpKernelConst ρ₁ η * geometricExpKernelConst ρ₂ η