The one-step averaged-flux estimate with both source errors retained.

theorem AVenhance.Infra.Section3.OneStepAveragingUnconditional.rpow_ceil_bounds_local {x : ℝ} (hx : 1 ≤ x) : x ≤ ↑⌈x⌉₊ ∧ ↑⌈x⌉₊ ≤ 2 * x

theorem AVenhance.Infra.Section3.OneStepAveragingUnconditional.tau_over_tauP_le_prev_delta {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) : tau β I.Λ m / tauP β I.Λ m ≤ epsilon β I.Λ (m - 1) ^ delta β / 4

theorem AVenhance.Infra.Section3.OneStepAveragingUnconditional.pow_le_self_of_unit_interval {x : ℝ} {n : ℕ} (hx0 : 0 ≤ x) (hx1 : x ≤ 1) (hn : 1 ≤ n) : x ^ n ≤ x

noncomputable def AVenhance.Infra.Section3.lAmtOneStepConstant (β C₀ : ℝ) : ℝ

Uniform coefficient in the unconditional one-step estimate.

Equations

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

theorem AVenhance.Infra.Section3.OneStepAveragingUnconditional.KhomScalar_one_step_error_small_uniform {β C₀ : ℝ} (I : Ingredients β) (hCz : I.Czeta ≤ C₀) (hCh : I.Chat ≤ C₀) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 < κ) (hsmall : epsilon β I.Λ m ^ 2 / (κ * tau β I.Λ m) ≤ 1 / 2) : have S := a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κ; have q := epsilon β I.Λ m ^ 2 / (κ * tau β I.Λ m); |I.KhomScalar κ m - (κ + 9 / 80 * S)| ≤ lAmtOneStepConstant β C₀ * S * (q + epsilon β I.Λ (m - 1) ^ delta β)

Small-ratio part of the one-step estimate, retaining both finite approximation losses and the cutoff-period contribution.

theorem AVenhance.Infra.Section3.KhomScalar_one_step_error_unconditional {β C₀ : ℝ} (I : Ingredients β) (hCz : I.Czeta ≤ C₀) (hCh : I.Chat ≤ C₀) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 < κ) : have S := a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κ; have q := epsilon β I.Λ m ^ 2 / (κ * tau β I.Λ m); |I.KhomScalar κ m - (κ + 9 / 80 * S)| ≤ lAmtOneStepConstant β C₀ * S * (q + epsilon β I.Λ (m - 1) ^ delta β)

One-step averaging estimate for the actual scalar flux, valid at every positive input diffusivity. It retains both finite-regularity losses and converts the cutoff-period loss to ε_(m-1)^δ; the large-ratio case follows from the pointwise flux cap.