The transition-window memory tail in the moving-cutoff energy.

theorem AVenhance.Infra.Section3.MovingFluxEnergy.xi_mem_Icc {β : ℝ} (I : Ingredients β) (t : ℝ) : 0 ≤ I.xi t ∧ I.xi t ≤ 1

theorem AVenhance.Infra.Section3.xiMK_odd_partition {β : ℝ} (I : Ingredients β) {m : ℕ} (_hm : 1 ≤ m) (t : ℝ) : ∑' (k : { k : ℤ // Odd k }), I.xiMK m (↑k) t = 1

The scaled odd transition cutoffs also form a nonnegative partition of unity.

theorem AVenhance.Infra.Section3.xiMK_mem_Icc {β : ℝ} (I : Ingredients β) {m : ℕ} (_hm : 1 ≤ m) (k : ℤ) (t : ℝ) : I.xiMK m k t ∈ Set.Icc 0 1

Every scaled transition cutoff lies in [0,1].

theorem AVenhance.Infra.Section3.xiMK_odd_support_finite {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (t : ℝ) : {k : { k : ℤ // Odd k } | I.xiMK m (↑k) t ≠ 0}.Finite

theorem AVenhance.Infra.Section3.xiMK_odd_sq_tsum_le_one {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (t : ℝ) : ∑' (k : { k : ℤ // Odd k }), I.xiMK m (↑k) t ^ 2 ≤ 1

The squared transition weights have total mass at most one.

noncomputable def AVenhance.Infra.Section3.movingCutoffMemoryEnergy {β : ℝ} (I : Ingredients β) (κ : ℝ) (m : ℕ) (t : ℝ) : ℝ

The cutoff-weighted memory square appearing in the diagonal moving energy.

Equations

• AVenhance.Infra.Section3.movingCutoffMemoryEnergy I κ m t = ∑' (k : { k : ℤ // Odd k }), I.xiMK m (↑k) t ^ 2 * I.corrTime κ m (↑k) t ^ 2

noncomputable def AVenhance.Infra.Section3.movingCutoffEnergyTrace {β : ℝ} (I : Ingredients β) (κ : ℝ) (m : ℕ) (t : ℝ) : ℝ

Trace of the nonnegative diagonal corrector-energy correction obtained by the source's active-shear gradient-square formula.

Equations

• AVenhance.Infra.Section3.movingCutoffEnergyTrace I κ m t = 8 * Real.pi ^ 4 * AVenhance.a β I.Λ m ^ 2 * κ * AVenhance.Infra.Section3.movingCutoffMemoryEnergy I κ m t

theorem AVenhance.Infra.Section3.MovingFluxEnergy.movingCutoffMemoryEnergy_summable {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ t : ℝ) : Summable fun (k : { k : ℤ // Odd k }) => I.xiMK m (↑k) t ^ 2 * I.corrTime κ m (↑k) t ^ 2

theorem AVenhance.Infra.Section3.movingCutoffMemoryEnergy_tail_bound {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (hκ : 0 < κ) (t : ℝ) (hforce : ∀ (k : { k : ℤ // Odd k }), I.zetaProd m (↑k) t = 0) : movingCutoffMemoryEnergy I κ m t ≤ ((I.Czeta + I.Chat) / tau β I.Λ m / (4 * Real.pi ^ 2 * κ / epsilon β I.Λ m ^ 2) ^ 2) ^ 2

If no small forcing window is active, every memory mode is in its transition tail. Its cutoff-weighted squared memory is bounded by the square of the one-mode relaxation error; the partition of unity sums these tails without an index-count loss.

theorem AVenhance.Infra.Section3.movingCutoffEnergyTrace_tail_bound {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (hκ : 0 < κ) (t : ℝ) (hforce : ∀ (k : { k : ℤ // Odd k }), I.zetaProd m (↑k) t = 0) (hcondition : epsilon β I.Λ m ^ 2 ≤ κ * tau β I.Λ m / 2) : movingCutoffEnergyTrace I κ m t ≤ (I.Czeta + I.Chat) ^ 2 / (64 * Real.pi ^ 4) * (a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κ) * (epsilon β I.Λ m ^ 2 / (κ * tau β I.Λ m))

In a transition window with no active forcing, the full nonnegative corrector-energy trace is quadratically small. Under the source condition ε_m² ≤ κ τ_m / 2, this implies the one-power error scale in l.flux.to.energy.

theorem AVenhance.Infra.Section3.movingCutoffEnergyTrace_tail_bound_uniform {β C₀ : ℝ} (I : Ingredients β) (hCz : I.Czeta ≤ C₀) (hCh : I.Chat ≤ C₀) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (hκ : 0 < κ) (t : ℝ) (hforce : ∀ (k : { k : ℤ // Odd k }), I.zetaProd m (↑k) t = 0) (hcondition : epsilon β I.Λ m ^ 2 ≤ κ * tau β I.Λ m / 2) : movingCutoffEnergyTrace I κ m t ≤ C₀ ^ 2 / (16 * Real.pi ^ 4) * (a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κ) * (epsilon β I.Λ m ^ 2 / (κ * tau β I.Λ m))

Uniform version of the inactive-window energy tail. Its constant is independent of the particular ingredient once the cutoff derivative fields are bounded by C₀.

theorem AVenhance.Infra.Section3.movingCutoffEnergyTrace_eq_active_mode {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (k : ℤ) (hk : Odd k) (t : ℝ) (hzk : I.zetaMK m k t ≠ 0) : movingCutoffEnergyTrace I κ m t = 8 * Real.pi ^ 4 * a β I.Λ m ^ 2 * κ * I.corrTime κ m k t ^ 2

When one small-scale forcing cutoff is active, the moving corrector-energy trace contains only that mode: its cutoff weight is one and every other odd transition weight is zero.

theorem AVenhance.Infra.Section3.movingFluxEnergy_active_entry_error {β C₀ : ℝ} (I : Ingredients β) (hCz : I.Czeta ≤ C₀) (hCh : I.Chat ≤ C₀) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (hκ : 0 < κ) (k : ℤ) (t : ℝ) (hk : k % 4 = 1 ∨ k % 4 = 3) (hzk : I.zetaMK m k t ≠ 0) : |(if k % 4 = 1 then I.flux κ m t 1 1 else I.flux κ m t 0 0) - κ - movingCutoffEnergyTrace I κ m t| ≤ (C₀ + C₀) / (4 * Real.pi ^ 2) * (a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / (2 * κ)) * (epsilon β I.Λ m ^ 2 / (κ * tau β I.Λ m))

The active diagonal flux entry differs from the moving corrector-energy trace by the cutoff-derivative error. The displayed constant is uniform over all ingredients whose two derivative constants are bounded by C₀.