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

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

Weighted superexponential kernels

The no-loss bad-scale proof keeps finite maxima as probability-level union prefactors. These prefactors are exponential in the summation variables, but the tail parameter is superexponential in the same variables. The kernels in this file absorb those finite-union weights without spending any power of the main bad scale.

noncomputable def HCPolySupport.Book.Ch05.Section57.weightedGeometricExpKernelConst (w R : ℝ) : ℝ

Sum of the geometrically weighted kernel w ^ k * exp (-(R ^ k - 1)).

Equations

• HCPolySupport.Book.Ch05.Section57.weightedGeometricExpKernelConst w R = ∑' (k : ℕ), w ^ k * Real.exp (-(R ^ k - 1))

noncomputable def HCPolySupport.Book.Ch05.Section57.weightedLinearExpKernelConst (w R : ℝ) : ℝ

Sum of the exponential kernel weighted by (k + 1) * w ^ k.

Equations

• HCPolySupport.Book.Ch05.Section57.weightedLinearExpKernelConst w R = ∑' (k : ℕ), (↑k + 1) * w ^ k * Real.exp (-(R ^ k - 1))

theorem HCPolySupport.Book.Ch05.Section57.summable_weightedLinearExpKernel {w R : ℝ} (hw : 0 < w) (hR : 1 < R) : Summable fun (k : ℕ) => (↑k + 1) * w ^ k * Real.exp (-(R ^ k - 1))

theorem HCPolySupport.Book.Ch05.Section57.summable_weightedGeometricExpKernel {w R : ℝ} (hw : 0 < w) (hR : 1 < R) : Summable fun (k : ℕ) => w ^ k * Real.exp (-(R ^ k - 1))

theorem HCPolySupport.Book.Ch05.Section57.weightedGeometricExpKernelConst_pos {w R : ℝ} (hw : 0 < w) (hR : 1 < R) : 0 < weightedGeometricExpKernelConst w R

theorem HCPolySupport.Book.Ch05.Section57.weightedLinearExpKernelConst_pos {w R : ℝ} (hw : 0 < w) (hR : 1 < R) : 0 < weightedLinearExpKernelConst w R

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

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

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

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

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