Weighted Convolution

theorem EulerWeightedConvolution.triangular_sum_le_product (N : ℕ) (a b : ℕ → ℝ) (ha : ∀ (n : ℕ), 0 ≤ a n) (hb : ∀ (n : ℕ), 0 ≤ b n) : ∑ n ∈ Finset.range (N + 1), ∑ l ∈ Finset.range n, a (l + 1) * b (n - l) ≤ (∑ l ∈ Finset.range (N + 1), a l) * ∑ j ∈ Finset.range (N + 1), b j

theorem EulerWeightedConvolution.external_commutator_term (ρ : ℝ) (hρ : 0 < ρ) (j l : ℕ) (hl : 1 ≤ l) (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) : EulerPacketWeights.weight ρ (j + l) * ↑((j + l).choose l) * a * b ≤ ρ⁻¹ * (EulerPacketWeights.weight ρ l * a) * (↑(j + 1) * EulerPacketWeights.weight ρ (j + 1) * b)

theorem EulerWeightedConvolution.external_commutator_sum (ρ : ℝ) (hρ : 0 < ρ) (N : ℕ) (a b : ℕ → ℝ) (ha : ∀ (n : ℕ), 0 ≤ a n) (hb : ∀ (n : ℕ), 0 ≤ b n) : ∑ n ∈ Finset.range (N + 1), ∑ l ∈ Finset.range n, EulerPacketWeights.weight ρ n * ↑(n.choose (l + 1)) * a (l + 1) * b (n - l) ≤ (ρ⁻¹ * ∑ l ∈ Finset.range (N + 1), EulerPacketWeights.weight ρ l * a l) * ∑ j ∈ Finset.range (N + 1), ↑j * EulerPacketWeights.weight ρ j * b j

The full truncated external-commutator convolution has a constant independent of the cutoff.

theorem EulerWeightedConvolution.shifted_triangular_sum_le_product (N : ℕ) (a b : ℕ → ℝ) (ha : ∀ (n : ℕ), 0 ≤ a n) (hb : ∀ (n : ℕ), 0 ≤ b n) : ∑ n ∈ Finset.range N, ∑ l ∈ Finset.range (n + 1), a l * b (n - l + 1) ≤ (2 * ∑ l ∈ Finset.range (N + 1), a l) * ∑ j ∈ Finset.range (N + 1), b j

theorem EulerWeightedConvolution.shifted_source_term (ρ : ℝ) (hρ : 0 < ρ) (j l : ℕ) (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) : ↑(j + l + 1) * EulerPacketWeights.weight ρ (j + l + 1) * ↑((j + l).choose l) * a * b ≤ EulerPacketWeights.weight ρ l * a * (↑(j + 1) * EulerPacketWeights.weight ρ (j + 1) * b)

theorem EulerWeightedConvolution.shifted_source_sum (ρ : ℝ) (hρ : 0 < ρ) (N : ℕ) (a b : ℕ → ℝ) (ha : ∀ (n : ℕ), 0 ≤ a n) (hb : ∀ (n : ℕ), 0 ≤ b n) : ∑ n ∈ Finset.range N, ∑ l ∈ Finset.range (n + 1), ↑(n + 1) * EulerPacketWeights.weight ρ (n + 1) * ↑(n.choose l) * a l * b (n - l + 1) ≤ (2 * ∑ l ∈ Finset.range (N + 1), EulerPacketWeights.weight ρ l * a l) * ∑ j ∈ Finset.range (N + 1), ↑j * EulerPacketWeights.weight ρ j * b j

The pressure-source derivative shift sums with a cutoff-independent constant.