Iterates Discharge Scalars

Support for the Armstrong–Vicol anomalous-diffusion formalization.

noncomputable def AVenhance.Infra.Section4.iterateMeanScaleConstant (β Ccut P : ℝ) : ℝ

The two averaging errors retain their distinct powers and constants.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Section4.iterate_discharge_smallness {x P L r : ℝ} (hx : 0 ≤ x) (hx1 : x ≤ 1) (hP : 0 ≤ P) (hL : 0 ≤ L) (hr : r ≤ P * x ^ 2) (hsmall : x ^ 2 ≤ (smallnessBudget 0 P L)⁻¹) : r ≤ 1 / 2 ∧ L * (r + x) ≤ 9 / 160

The same squared coefficient budget controls the terminal-aware ratio and one-step averaging error. Its inputs are scalar coefficients, not PDE bounds.

theorem AVenhance.Infra.Section4.iterate_two_error_mean_scale {e δ κprev B A D P r h : ℝ} {N : ℕ} (he : 0 < e) (he1 : e ≤ 1) (hδ : 0 < δ) (hN : 2 ≤ N) (hκ : 0 ≤ κprev) (hA : 0 ≤ A) (hD : 0 ≤ D) (hP : 0 ≤ P) (hr : 0 ≤ r) (hrP : r ≤ P * e ^ (2 * δ)) (hh : 0 ≤ h) (hhP : h ≤ 1 / 4 * e ^ δ) (hsize : B ≤ 160 / 9 * κprev) : B * (A * r ^ N + D * h ^ N) ≤ κprev * (160 / 9 * (A * P ^ N + D * (1 / 4) ^ N)) * e ^ (2 * δ)

Both finite-average error powers have the required rho gain.

theorem AVenhance.Infra.Section4.iterate_discharge_threshold_from_source {C₀ D ρ : ℝ} (hC : 1 ≤ C₀) (hDp : 0 < D) (hD : D ≤ C₀) (hsmall : ρ ≤ (4 * C₀ ^ 3)⁻¹) : ρ ≤ D⁻¹

Enlarging the l.V constant absorbs the cheap-input threshold without an additional data-dependent smallness parameter.