Iterates Discharge Chain

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_chain_mean_scale {β Ccut P κ : ℝ} (I : Ingredients β) (hz : I.Czeta ≤ Ccut) (hh : I.Chat ≤ Ccut) (hP : 0 ≤ P) {m M : ℕ} (hm : 1 ≤ m) (hκ : 0 < κ) (hratio : epsilon β I.Λ m ^ 2 / (I.kappaAt κ m (M - m) * tau β I.Λ m) ≤ P * epsilon β I.Λ (m - 1) ^ (2 * delta β)) (hsize : I.kappaAt κ m (M - m) + a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / I.kappaAt κ m (M - m) ≤ 160 / 9 * I.kappaAt κ (m - 1) (M - (m - 1))) : iterateMeanErrorBound I (I.kappaAt κ m (M - m)) m ≤ I.kappaAt κ (m - 1) (M - (m - 1)) * iterateMeanScaleConstant β Ccut P * epsilon β I.Λ (m - 1) ^ (2 * delta β)

The explicit E21c TWO-error mean comparison has the required rho scale.