Exact zeroth-order cutoff average used in the Section 3 one-step estimate.

theorem AVenhance.Infra.Section3.OneStepAveraging.zetaMK_coord_of_ne_zero {β : ℝ} (I : Ingredients β) {m : ℕ} (_hm : 1 ≤ m) {k : ℤ} {t : ℝ} (hz : I.zetaMK m k t ≠ 0) : (t - ↑k * tau β I.Λ m) / tau β I.Λ m ∈ Set.Icc (-(2 / 3)) (2 / 3)

theorem AVenhance.Infra.Section3.OneStepAveraging.zetaMK_cell_centers {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {k : ℤ} {t : ℝ} (ht : t ∈ Set.Icc 0 (4 * tau β I.Λ m)) (hk : Odd k) (hz : I.zetaMK m k t ≠ 0) : k = 1 ∨ k = 3

On [0,4τ_m], a nonzero small cutoff can only have center τ_m or 3τ_m.

theorem AVenhance.Infra.Section3.OneStepAveraging.zetaMK_square_cell_integral {β : ℝ} (I : Ingredients β) {m : ℕ} (_hm : 1 ≤ m) (r : ℤ) (hr : r = 1 ∨ r = 3) : ∫ (t : ℝ) in 0..4 * tau β I.Λ m, I.zetaMK m r t ^ 2 = tau β I.Λ m * (9 / 10)

The integral of a scaled cutoff over a four-cell period is the prescribed 9/10 mass of the original cutoff.

def AVenhance.Infra.Section3.OneStepAveraging.shearModeOne : Matrix (Fin 2) (Fin 2) ℝ

Diagonal projector onto the second coordinate for the first shear mode.

Equations

• AVenhance.Infra.Section3.OneStepAveraging.shearModeOne = !![0, 0; 0, 1]

def AVenhance.Infra.Section3.OneStepAveraging.shearModeThree : Matrix (Fin 2) (Fin 2) ℝ

Diagonal projector onto the first coordinate for the third shear mode.

Equations

• AVenhance.Infra.Section3.OneStepAveraging.shearModeThree = !![1, 0; 0, 0]

theorem AVenhance.Infra.Section3.OneStepAveraging.jMN_zero_two_mode_formula {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ t : ℝ) (ht : t ∈ Set.Icc 0 (4 * tau β I.Λ m)) : I.jMN κ m 0 t = (2 * Real.pi ^ 2 * a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 2) • (I.zetaMK m 1 t ^ 2 • shearModeOne + I.zetaMK m 3 t ^ 2 • shearModeThree)

During a four-cell period, the order-zero shear flux has only the two modes centered at cells one and three.

theorem AVenhance.Infra.Section3.jMN_zero_average_eq {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) : timeAvgMat (I.jMN κ m 0) = (9 * Real.pi ^ 2 / 20 * a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 2) • 1

Exact period average of the order-zero oscillatory flux.

theorem AVenhance.Infra.Section3.OneStepAveraging.expShift_integrableOn_Iic {ρ t : ℝ} (hρ : 0 < ρ) : MeasureTheory.IntegrableOn (fun (s : ℝ) => Real.exp (ρ * (s - t))) (Set.Iic t) MeasureTheory.volume

theorem AVenhance.Infra.Section3.OneStepAveraging.expShift_integral_Iic {ρ t : ℝ} (hρ : 0 < ρ) : ∫ (s : ℝ) in Set.Iic t, Real.exp (ρ * (s - t)) = ρ⁻¹

theorem AVenhance.Infra.Section3.OneStepAveraging.hatZeta_memory_integrable {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (l : ℤ) {ρ t : ℝ} (hρ : 0 < ρ) : MeasureTheory.IntegrableOn (fun (s : ℝ) => I.hatZetaML m l s * Real.exp (ρ * (s - t))) (Set.Iic t) MeasureTheory.volume

theorem AVenhance.Infra.Section3.OneStepAveraging.hatZeta_memory_bounds {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (l : ℤ) {ρ t : ℝ} (hρ : 0 < ρ) : 0 ≤ ∫ (s : ℝ) in Set.Iic t, I.hatZetaML m l s * Real.exp (ρ * (s - t)) ∧ ∫ (s : ℝ) in Set.Iic t, I.hatZetaML m l s * Real.exp (ρ * (s - t)) ≤ ρ⁻¹

theorem AVenhance.Infra.Section3.OneStepAveraging.hatZetaML_eq_one_on_core {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (l : ℤ) (T P t : ℝ) (ht : t ∈ Set.Icc ((↑l - 1 / 2) * T + 2 * P) ((↑l + 1 / 2) * T - 2 * P)) (hT : T = tauPP β I.Λ m) (hP : P = tauP β I.Λ m) : I.hatZetaML m l t = 1

theorem AVenhance.Infra.Section3.OneStepAveraging.LMN_zero_nonneg {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (hκ : 0 < κ) (t : ℝ) : 0 ≤ I.LMN κ m 0 t

theorem AVenhance.Infra.Section3.OneStepAveraging.LMN_zero_le_inv {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (hκ : 0 < κ) (t : ℝ) : I.LMN κ m 0 t ≤ (4 * Real.pi ^ 2 * κ / epsilon β I.Λ m ^ 2)⁻¹

theorem AVenhance.Infra.Section3.OneStepAveraging.LMN_zero_ge_core {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (hκ : 0 < κ) (T P t : ℝ) (hT : T = tauPP β I.Λ m) (hP : P = tauP β I.Λ m) (ht : t ∈ Set.Icc (-(T / 2) + 3 * P) (T / 2 - 2 * P)) : (1 - Real.exp (-(4 * Real.pi ^ 2 * κ / epsilon β I.Λ m ^ 2) * P)) / (4 * Real.pi ^ 2 * κ / epsilon β I.Λ m ^ 2) ≤ I.LMN κ m 0 t

theorem AVenhance.Infra.Section3.LMN_zero_unit_average_bounds {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (hκ : 0 < κ) : have T := tauPP β I.Λ m; have P := tauP β I.Λ m; have ρ := 4 * Real.pi ^ 2 * κ / epsilon β I.Λ m ^ 2; 0 ≤ ∫ (t : ℝ) in 0..1, I.LMN κ m 0 t ∧ ∫ (t : ℝ) in 0..1, I.LMN κ m 0 t ≤ ρ⁻¹ ∧ 1 / T * (T - 5 * P) * ((1 - Real.exp (-ρ * P)) / ρ) ≤ ∫ (t : ℝ) in 0..1, I.LMN κ m 0 t

Period averaging bounds the zeroth memory coefficient from above by the full relaxation scale and from below by the contribution of the plateau.

theorem AVenhance.Infra.Section3.LMN_zero_unit_average_error {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (hκ : 0 < κ) : |(∫ (t : ℝ) in 0..1, I.LMN κ m 0 t) - (4 * Real.pi ^ 2 * κ / epsilon β I.Λ m ^ 2)⁻¹| ≤ (4 * Real.pi ^ 2 * κ / epsilon β I.Λ m ^ 2)⁻¹ * (5 * tauP β I.Λ m / tauPP β I.Λ m + Real.exp (-(4 * Real.pi ^ 2 * κ / epsilon β I.Λ m ^ 2) * tauP β I.Λ m))

Quantitative error of the zeroth memory average from its full relaxation integral. The two losses are the fraction of the large period outside the cutoff plateau and the residual exponential memory before that plateau.

theorem AVenhance.Infra.Section3.timeAvgMat_Kmat_entry_formula {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (hκ : 0 < κ) (i j : Fin 2) : timeAvgMat (I.Kmat κ m) i j = (κ * if i = j then 1 else 0) + ∑ n ∈ Finset.range (Nstar β), (∫ (t : ℝ) in 0..1, I.LMN κ m n t) * timeAvgMat (I.jMN κ m n) i j

theorem AVenhance.Infra.Section3.LMN_unit_average_abs_le {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 < κ) (n : ℕ) : |∫ (t : ℝ) in 0..1, I.LMN κ m n t| ≤ ↑n.factorial * 2 ^ n * (4 * Real.pi ^ 2 * κ / epsilon β I.Λ m ^ 2 / 2)⁻¹

Integrating the explicit L_mn envelope preserves its pointwise bound. This is the scalar ingredient used in the nonzero-order tail of the one-step averaging estimate.

theorem AVenhance.Infra.Section3.OneStepAveraging.LMN_jMN_unit_average_product_le {β : ℝ} (I : Ingredients β) {m n : ℕ} (hm : 1 ≤ m) (hn : 0 < n) (hN : n ≤ Nstar β) {κ : ℝ} (hκ : 0 < κ) (hcondition : epsilon β I.Λ m ^ 2 ≤ κ * tau β I.Λ m / 2) : |(∫ (t : ℝ) in 0..1, I.LMN κ m n t) * timeAvgMat (I.jMN κ m n) 0 0| ≤ I.Czeta * a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κ * (2 * epsilon β I.Λ m ^ 2 / (4 * Real.pi ^ 2 * κ * tau β I.Λ m))

theorem AVenhance.Infra.Section3.Kmat_average_one_step_error {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 < κ) (hcondition : epsilon β I.Λ m ^ 2 ≤ κ * tau β I.Λ m / 2) : |timeAvgMat (I.Kmat κ m) 0 0 - (κ + 9 / 80 * (a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κ))| ≤ 9 / 80 * (a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κ) * (5 * tauP β I.Λ m / tauPP β I.Λ m + Real.exp (-(4 * Real.pi ^ 2 * κ / epsilon β I.Λ m ^ 2) * tauP β I.Λ m)) + ↑(Nstar β) * (I.Czeta * a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κ) * (2 * epsilon β I.Λ m ^ 2 / (4 * Real.pi ^ 2 * κ * tau β I.Λ m))

One-step estimate for the average of the Kmat. The zeroth mode produces the 9/80 increment; all positive orders form a geometric tail under the source small-ratio condition.

theorem AVenhance.Infra.Section3.KhomScalar_one_step_error_finite {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 < κ) (hcondition : epsilon β I.Λ m ^ 2 ≤ κ * tau β I.Λ m / 2) : |I.KhomScalar κ m - (κ + 9 / 80 * (a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κ))| ≤ 9 / 80 * (a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κ) * (5 * tauP β I.Λ m / tauPP β I.Λ m + Real.exp (-(4 * Real.pi ^ 2 * κ / epsilon β I.Λ m ^ 2) * tauP β I.Λ m)) + ↑(Nstar β) * (I.Czeta * a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κ) * (2 * epsilon β I.Λ m ^ 2 / (4 * Real.pi ^ 2 * κ * tau β I.Λ m)) + a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κ * (4 * Real.pi ^ 2 * I.Czeta * ↑(Nstar β) * 2 ^ Nstar β * (epsilon β I.Λ m ^ 2 / (κ * tau β I.Λ m)) ^ Nstar β + 2 * ↑(Nstar β) * I.Czeta * ↑(Nstar β).factorial * 2 ^ Nstar β * 2 ^ Nstar β * I.Chat ^ 2 * 8 ^ Nstar β * (tau β I.Λ m / tauP β I.Λ m) ^ Nstar β)

One-step estimate for the actual averaged flux KhomScalar, retaining both justified finite-regularity errors from Approx.lean. The extra (tau/tauP)^Nstar term is not silently replaced by the q^Nstar term.

theorem AVenhance.Infra.Section3.KhomScalar_one_step_error_finite_uniform {β C₀ : ℝ} (I : Ingredients β) (hCz : I.Czeta ≤ C₀) (hCh : I.Chat ≤ C₀) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 < κ) (hcondition : epsilon β I.Λ m ^ 2 ≤ κ * tau β I.Λ m / 2) : |I.KhomScalar κ m - (κ + 9 / 80 * (a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κ))| ≤ 9 / 80 * (a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κ) * (5 * tauP β I.Λ m / tauPP β I.Λ m + Real.exp (-(4 * Real.pi ^ 2 * κ / epsilon β I.Λ m ^ 2) * tauP β I.Λ m)) + ↑(Nstar β) * (C₀ * a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κ) * (2 * epsilon β I.Λ m ^ 2 / (4 * Real.pi ^ 2 * κ * tau β I.Λ m)) + a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κ * (4 * Real.pi ^ 2 * C₀ * ↑(Nstar β) * 2 ^ Nstar β * (epsilon β I.Λ m ^ 2 / (κ * tau β I.Λ m)) ^ Nstar β + 2 * ↑(Nstar β) * C₀ * ↑(Nstar β).factorial * 2 ^ Nstar β * 2 ^ Nstar β * C₀ ^ 2 * 8 ^ Nstar β * (tau β I.Λ m / tauP β I.Λ m) ^ Nstar β)

Ingredient-uniform form of the one-step estimate under the cutoff bounds used by the diffusivity-recursion estimate. Its constants depend on β and C₀, not on the chosen I.