Exact shifted factorial profiles for differentiated material forcing.

theorem AVenhance.Infra.Section4.iterate_weighted_shifted_factorial_term_le (n j a : ℕ) (hj : j ≤ n) {b L : ℝ} (hL : 0 < L) : ↑(n.choose j) ^ 2 * 2 ^ j * (↑j.factorial * b ^ j) ^ 2 * (↑(n - j + a).factorial * L ^ (n - j)) ^ 2 ≤ (2 * (b / L) ^ 2) ^ j * (↑(n + a).factorial * L ^ n) ^ 2

Squared cancellation at an arbitrary shifted scalar factorial.

theorem AVenhance.Infra.Section4.iterate_forcing_factorial_profile_sum_le (n a : ℕ) {b L : ℝ} (hL : 0 < L) (hg : 2 * (b / L) ^ 2 ≤ 1 / 2) : ∑ j ∈ Finset.range (n + 1), ↑(n.choose j) ^ 2 * 2 ^ j * (↑j.factorial * b ^ j) ^ 2 * (↑(n - j + a).factorial * L ^ (n - j)) ^ 2 ≤ 2 * (↑(n + a).factorial * L ^ n) ^ 2

The full shifted factorial sum has a constant bound, including order zero.