Iterates Finite Analytic Sum

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_amplitude_le_half_pow {η : ℝ} (hη : 0 ≤ η) (hsmall : η ≤ 1 / 4) (i : ℕ) : iterateAmplitude η i ≤ (1 / 2) ^ i

The printed amplitudes have a geometric majorant at the T threshold.

theorem AVenhance.Infra.Section4.iterate_amplitude_four_sum {η : ℝ} (hη : 0 ≤ η) (hsmall : η ≤ 1 / 4) (N : ℕ) : ∑ i ∈ Finset.range (N + 1), iterateAmplitude η i * 4 ^ i ≤ 4 ^ N

The finite weighted sum supplies precisely the printed 2^(2N) constant.

theorem AVenhance.Infra.Section4.iterate_factorial_shift_bound (n N : ℕ) {i : ℕ} (hi : i ≤ N) : ↑(n + 2 * i).factorial ≤ ↑n.factorial * ↑(2 * N).factorial * 2 ^ n * 4 ^ i

A factorial shift costs a binomial power and the finite terminal factorial.

theorem AVenhance.Infra.Section4.iterate_finite_analytic_sum {η L : ℝ} (hη : 0 ≤ η) (hsmall : η ≤ 1 / 4) (hL : 0 ≤ L) (n N : ℕ) : ∑ i ∈ Finset.range (N + 1), iterateAmplitude η i * ↑(n + 2 * i).factorial * L ^ n ≤ 4 ^ N * ↑(2 * N).factorial * ↑n.factorial * (2 * L) ^ n

Analytic finite-sum bound for the printed increment weights.

theorem AVenhance.Infra.Section4.iterate_amplitude_le_parameter {η : ℝ} (hη : 0 ≤ η) (hη1 : η ≤ 1) {i : ℕ} (hi : 1 ≤ i) : iterateAmplitude η i ≤ η

Every positive correction amplitude is at most the small parameter.

theorem AVenhance.Infra.Section4.iterate_finite_gradient_amplitude_sum {η : ℝ} (hη : 0 ≤ η) (hη1 : η ≤ 1) (N : ℕ) : ∑ i ∈ Finset.range (N + 1), iterateAmplitude η i * ↑(2 * i).factorial ≤ 1 + η * ↑N * ↑(2 * N).factorial

A gradient-only finite T sum is one base amplitude plus small corrections.