Appendix B.2 transport estimates

This module records the numerical estimates used in the transport induction. The corrected coefficient is kept in its source-correct form; its equal-radius specialization is the one consumed by the paper's later application.

theorem AVenhance.FaaDiBruno.transportE18_equalRadius_le_eighth {n : ℕ} {d C_f R_f t : ℝ} (hd : 1 ≤ d) (hCf : 0 < C_f) (hRf : 0 < R_f) (ht : 0 ≤ t) (hT : t ≤ 1 / (4 * d * C_f * R_f)) : ↑n * (R_f + 4 * t * d * C_f * R_f ^ 2) / (16 * (↑n + 1) * R_f) ≤ 1 / 8

For equal forcing and transport radii, the corrected coefficient is at most 1/8 throughout the time interval in (10578).

theorem AVenhance.FaaDiBruno.transportE18_equalRadius_absorption {d C_g S : ℝ} (hd : 1 ≤ d) (hCg : 0 ≤ C_g) (hS : S ≤ C_g + S / 8 + 6 * d * C_g) : S ≤ 8 * d * C_g

The absorption step in Lemma 10577 after the correction, when R_g = R_f and hence the coefficient is bounded by 1/8.

theorem AVenhance.FaaDiBruno.transportRadiusIntegral_bound {j : ℕ} {d C_f R_f R_g t : ℝ} (hd : 0 < d) (hCf : 0 < C_f) (hRf : 0 < R_f) (hRg : 0 ≤ R_g) (ht : 0 ≤ t) : ∫ (s : ℝ) in 0..t, s * (R_g + 4 * d * C_f * R_f ^ 2 * s) ^ j ≤ t * (R_g + 4 * d * C_f * R_f ^ 2 * t) ^ (j + 1) / (4 * d * C_f * R_f ^ 2 * (↑j + 1))

The radius integral estimate (10650), with the affine radius written explicitly. The proof uses s ≤ t and integrates the exact power primitive.

theorem AVenhance.FaaDiBruno.Transport.reciprocalSquareShift_le (c m : ℕ) (hc : 2 ≤ c) : ∑ k ∈ Finset.range m, 1 / (↑k + ↑c) ^ 2 ≤ 1 / (↑c - 1)

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

The corrected shifted reciprocal-square sum used at (10660) is at most 3/2. The unshifted (k+1)^{-2} version printed at (10663) is false.

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

The time-space convolution used in the induction for Lemma 10698. The (k+2) shift makes it bounded by the Appendix B product convolution.