Product estimates for the Appendix B seminorm

theorem AVenhance.FaaDiBruno.derivativeSup_mul_le {d n : ℕ} [Nonempty (Fin d)] (f g : Homogenization.Vec d → ℝ) (hf : ContDiff ℝ (↑n) f) (hg : ContDiff ℝ (↑n) g) : (derivativeSup n fun (x : Homogenization.Vec d) => f x * g x) ≤ ∑ k ∈ Finset.range (n + 1), ↑(n.choose k) * derivativeSup k f * derivativeSup (n - k) g

The coordinate derivative seminorm of a product is bounded by the binomial convolution of the two derivative seminorms.

noncomputable def AVenhance.FaaDiBruno.Product.harmonicOne (m : ℕ) : ℝ

Sum of the reciprocals of the first positive integers up to the given order.

Equations

• AVenhance.FaaDiBruno.Product.harmonicOne m = ∑ k ∈ Finset.range m, (↑k + 1)⁻¹

noncomputable def AVenhance.FaaDiBruno.Product.harmonicTwo (m : ℕ) : ℝ

Sum of the reciprocal squares of the first positive integers up to the given order.

Equations

• AVenhance.FaaDiBruno.Product.harmonicTwo m = ∑ k ∈ Finset.range m, ((↑k + 1) ^ 2)⁻¹

theorem AVenhance.FaaDiBruno.Product.weightedConvolution_identity (m : ℕ) : ∑ k ∈ Finset.range m, ↑m ^ 2 / ((↑k + 1) ^ 2 * (↑m - ↑k) ^ 2) = (↑m / (↑m + 1)) ^ 2 * (2 * harmonicTwo m + 4 * harmonicOne m / (↑m + 1))

theorem AVenhance.FaaDiBruno.Product.tailReciprocalSquares (q : ℕ) : ∑ k ∈ Finset.range q, ((↑k + 6) ^ 2)⁻¹ ≤ 1 / 5

theorem AVenhance.FaaDiBruno.Product.harmonicTwo_le_five_thirds (m : ℕ) : harmonicTwo m ≤ 5 / 3

theorem AVenhance.FaaDiBruno.Product.harmonicOne_nonneg (m : ℕ) : 0 ≤ harmonicOne m

theorem AVenhance.FaaDiBruno.Product.harmonicOne_sq_le (m : ℕ) : harmonicOne m ^ 2 ≤ ↑m * harmonicTwo m

theorem AVenhance.FaaDiBruno.Product.harmonicOne_sqrt_bound {m : ℕ} (hm : 32 ≤ m) : √(5 * ↑m / 3) ≤ ↑m / 6 + 2

theorem AVenhance.FaaDiBruno.Product.weightedConvolution_bound_large {m : ℕ} (hm : 32 ≤ m) : (↑m / (↑m + 1)) ^ 2 * (2 * harmonicTwo m + 4 * harmonicOne m / (↑m + 1)) ≤ 4

theorem AVenhance.FaaDiBruno.Product.weightedConvolution_le_four (m : ℕ) : ∑ k ∈ Finset.range m, ↑m ^ 2 / ((↑k + 1) ^ 2 * (↑m - ↑k) ^ 2) ≤ 4

theorem AVenhance.FaaDiBruno.weightedConvolution_le_four_paper (n : ℕ) : ∑ k ∈ Finset.range (n + 1), (↑n + 1) ^ 2 / ((↑k + 1) ^ 2 * ↑(n - k + 1) ^ 2) ≤ 4

The scalar weight sum in the paper's product estimate is at most four.

theorem AVenhance.FaaDiBruno.Product.weightedCoefficient_identity {n k : ℕ} (hk : k ≤ n) (R : ℝ) : have r := (ENNReal.ofReal R)⁻¹; ENNReal.ofReal ((↑n + 1) ^ 2 / ↑n.factorial) * r ^ n * ENNReal.ofReal ↑(n.choose k) = ENNReal.ofReal ((↑n + 1) ^ 2 / ((↑k + 1) ^ 2 * ↑(n - k + 1) ^ 2)) * (ENNReal.ofReal ((↑k + 1) ^ 2 / ↑k.factorial) * r ^ k) * (ENNReal.ofReal (↑(n - k + 1) ^ 2 / ↑(n - k).factorial) * r ^ (n - k))

theorem AVenhance.FaaDiBruno.snorm_mul_le_weightedSum {d n : ℕ} [Nonempty (Fin d)] (f g : Homogenization.Vec d → ℝ) (hf : ContDiff ℝ (↑n) f) (hg : ContDiff ℝ (↑n) g) (R : ℝ) : snorm (fun (x : Homogenization.Vec d) => f x * g x) n R ≤ ∑ k ∈ Finset.range (n + 1), ENNReal.ofReal ((↑n + 1) ^ 2 / ((↑k + 1) ^ 2 * ↑(n - k + 1) ^ 2)) * snorm f k R * snorm g (n - k) R

The product seminorm is bounded by the weighted binomial convolution before applying the numerical factor-four estimate.

noncomputable def AVenhance.FaaDiBruno.snormMax {d : ℕ} (f : Homogenization.Vec d → ℝ) (n : ℕ) (R : ℝ) : ENNReal

The finite maximum of the seminorms of orders zero through n.

Equations

• AVenhance.FaaDiBruno.snormMax f n R = ⨆ (j : Fin (n + 1)), AVenhance.FaaDiBruno.snorm f (↑j) R

theorem AVenhance.FaaDiBruno.productEstimate {d n : ℕ} [Nonempty (Fin d)] (f g : Homogenization.Vec d → ℝ) (hf : ContDiff ℝ (↑n) f) (hg : ContDiff ℝ (↑n) g) {R : ℝ} (_hR : 0 < R) : snorm (fun (x : Homogenization.Vec d) => f x * g x) n R ≤ 4 * snormMax f n R * snormMax g n R

The full product estimate of Appendix B.1, with the paper's constant.

theorem AVenhance.FaaDiBruno.Product.derivativeSup_zero {d : ℕ} (f : Homogenization.Vec d → ℝ) : derivativeSup 0 f = MeasureTheory.eLpNormEssSup f (vecVolume d)

The zeroth-order derivative seminorm is the essential supremum of the function itself.