Matrix-valued flux comparison with the mode-reduced moving energy.

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

The spatially averaged gradient energy of one shear mode.

Equations

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

def AVenhance.Infra.Section3.MovingFluxEnergyComplete.movingEnergyCoordinate (k : ℤ) : Fin 2

Spatial coordinate selected by the moving-energy shear index.

Equations

• AVenhance.Infra.Section3.MovingFluxEnergyComplete.movingEnergyCoordinate k = if k % 4 = 1 then 1 else 0

def AVenhance.Infra.Section3.MovingFluxEnergyComplete.movingEnergyCoordinateActive (i : Fin 2) (k : ℤ) : Bool

Decide whether a coordinate is the active coordinate of a moving-energy shear mode.

Equations

• AVenhance.Infra.Section3.MovingFluxEnergyComplete.movingEnergyCoordinateActive i k = decide (i = AVenhance.Infra.Section3.MovingFluxEnergyComplete.movingEnergyCoordinate k)

noncomputable def AVenhance.Infra.Section3.MovingFluxEnergyComplete.movingEnergyModeTerm {β : ℝ} (I : Ingredients β) (κ : ℝ) (m : ℕ) (t : ℝ) (k : { k : ℤ // Odd k }) : ℝ

Cutoff-weighted contribution of an odd shear mode to the moving energy.

Equations

• AVenhance.Infra.Section3.MovingFluxEnergyComplete.movingEnergyModeTerm I κ m t k = I.xiMK m (↑k) t ^ 2 * AVenhance.Infra.Section3.movingEnergyModeCoefficient I κ m (↑k) t

noncomputable def AVenhance.Infra.Section3.movingEnergyGramMean {β : ℝ} (I : Ingredients β) (κ : ℝ) (m : ℕ) (k : ℤ) (t : ℝ) : Matrix (Fin 2) (Fin 2) ℝ

Entrywise spatial average of one mode's gradient Gram matrix.

Equations

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

theorem AVenhance.Infra.Section3.MovingFluxEnergyComplete.movingEnergyGram_horizontal {β : ℝ} (I : Ingredients β) {m : ℕ} (κ : ℝ) (k : ℤ) (t : ℝ) (hk : k % 4 = 1) (x : Homogenization.Vec 2) : (gradMatrix (I.chiMK κ m k t) x).transpose * gradMatrix (I.chiMK κ m k t) x = spaceGrad (fun (y : Homogenization.Vec 2) => I.chiMK κ m k t y 1) x 0 ^ 2 • Matrix.single 1 1 1

theorem AVenhance.Infra.Section3.MovingFluxEnergyComplete.movingEnergyGram_vertical {β : ℝ} (I : Ingredients β) {m : ℕ} (κ : ℝ) (k : ℤ) (t : ℝ) (hk : k % 4 = 3) (x : Homogenization.Vec 2) : (gradMatrix (I.chiMK κ m k t) x).transpose * gradMatrix (I.chiMK κ m k t) x = spaceGrad (fun (y : Homogenization.Vec 2) => I.chiMK κ m k t y 0) x 1 ^ 2 • Matrix.single 0 0 1

theorem AVenhance.Infra.Section3.movingEnergyGramMean_horizontal {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (k : ℤ) (t : ℝ) (hk : k % 4 = 1) : movingEnergyGramMean I κ m k t = (8 * Real.pi ^ 4 * a β I.Λ m ^ 2 * I.corrTime κ m k t ^ 2) • Matrix.single 1 1 1

The horizontal shear contributes only its active diagonal energy entry.

theorem AVenhance.Infra.Section3.movingEnergyGramMean_vertical {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (k : ℤ) (t : ℝ) (hk : k % 4 = 3) : movingEnergyGramMean I κ m k t = (8 * Real.pi ^ 4 * a β I.Λ m ^ 2 * I.corrTime κ m k t ^ 2) • Matrix.single 0 0 1

The vertical shear contributes only its active diagonal energy entry.

noncomputable def AVenhance.Infra.Section3.movingCutoffEnergyCorrectionEntry {β : ℝ} (I : Ingredients β) (κ : ℝ) (m : ℕ) (t : ℝ) (i : Fin 2) : ℝ

The mode-reduced spatial energy correction in coordinate i.

Equations

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

theorem AVenhance.Infra.Section3.movingCutoffEnergyCorrectionEntry_eq_spatial_mode_sum {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ t : ℝ) (i : Fin 2) : movingCutoffEnergyCorrectionEntry I κ m t i = ∑' (k : { k : ℤ // Odd k }), I.xiMK m (↑k) t ^ 2 * κ * movingEnergyGramMean I κ m (↑k) t i i

The diagonal energy correction is exactly the sum of the spatially averaged single-mode gradient Gram entries. This identifies the diagonal energy matrix used in the flux estimate with the source's E_m formula after the finite-support double-sum reduction.

noncomputable def AVenhance.Infra.Section3.movingCutoffEnergyMatrix {β : ℝ} (I : Ingredients β) (κ : ℝ) (m : ℕ) (t : ℝ) : Matrix (Fin 2) (Fin 2) ℝ

The moving energy after the double-sum orthogonality reduction. Its molecular part is κ I; its modewise correction is diagonal.

Equations

• AVenhance.Infra.Section3.movingCutoffEnergyMatrix I κ m t = κ • 1 + Matrix.diagonal (AVenhance.Infra.Section3.movingCutoffEnergyCorrectionEntry I κ m t)

theorem AVenhance.Infra.Section3.movingCutoffEnergyMatrix_eq_spatial_mode_sum {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ t : ℝ) : movingCutoffEnergyMatrix I κ m t = κ • 1 + Matrix.diagonal fun (i : Fin 2) => ∑' (k : { k : ℤ // Odd k }), I.xiMK m (↑k) t ^ 2 * κ * movingEnergyGramMean I κ m (↑k) t i i

Matrix form of the diagonal source energy after the double-sum reduction: each diagonal correction is the sum of the spatial averages of the mode Gram entries, and the molecular baseline is κ I.

noncomputable def AVenhance.Infra.Section3.movingEnergyReducedSourceMatrix {β : ℝ} (I : Ingredients β) (κ : ℝ) (m : ℕ) (t : ℝ) (S : Finset { k : ℤ // Odd k }) : Matrix (Fin 2) (Fin 2) ℝ

Finite-support version of the source energy after the overlap reduction. The diagonal terms are the spatial means of the single-mode Gram matrices.

Equations

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

theorem AVenhance.Infra.Section3.movingCutoffEnergyMatrix_eq_source_reduced {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ t : ℝ) : have S := ⋯.toFinset; movingCutoffEnergyMatrix I κ m t = movingEnergyReducedSourceMatrix I κ m t S

For the actual finite cutoff support, the source's spatially averaged diagonal energy formula agrees with the mode-trace matrix used in the flux estimate. Together with movingEnergy_double_sum_reduces, this closes the finite E_m double-sum reduction.

theorem AVenhance.Infra.Section3.MovingFluxEnergyComplete.movingEnergyModeTerm_summable {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ t : ℝ) : Summable (movingEnergyModeTerm I κ m t)

theorem AVenhance.Infra.Section3.MovingFluxEnergyComplete.movingEnergyCorrectionEntry_summable {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ t : ℝ) (i : Fin 2) : Summable fun (k : { k : ℤ // Odd k }) => if movingEnergyCoordinateActive i ↑k = true then movingEnergyModeTerm I κ m t k else 0

theorem AVenhance.Infra.Section3.MovingFluxEnergyComplete.movingCutoffEnergyTrace_eq_tsum_modeTerm {β : ℝ} (I : Ingredients β) {m : ℕ} (_hm : 1 ≤ m) (κ t : ℝ) : movingCutoffEnergyTrace I κ m t = ∑' (k : { k : ℤ // Odd k }), movingEnergyModeTerm I κ m t k

theorem AVenhance.Infra.Section3.MovingFluxEnergyComplete.movingEnergyModeTerm_nonneg {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (hκ : 0 < κ) (t : ℝ) (k : { k : ℤ // Odd k }) : 0 ≤ movingEnergyModeTerm I κ m t k

theorem AVenhance.Infra.Section3.movingCutoffEnergyCorrectionEntry_bounds {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (hκ : 0 < κ) (t : ℝ) (i : Fin 2) : 0 ≤ movingCutoffEnergyCorrectionEntry I κ m t i ∧ movingCutoffEnergyCorrectionEntry I κ m t i ≤ movingCutoffEnergyTrace I κ m t

Each coordinate correction is nonnegative and bounded by the full trace.

theorem AVenhance.Infra.Section3.MovingFluxEnergyComplete.movingCutoffEnergyCorrectionEntry_active {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (k : ℤ) (hk : k % 4 = 1 ∨ k % 4 = 3) (t : ℝ) (hzk : I.zetaMK m k t ≠ 0) (i : Fin 2) : movingCutoffEnergyCorrectionEntry I κ m t i = if movingEnergyCoordinateActive i k = true then movingCutoffEnergyTrace I κ m t else 0

theorem AVenhance.Infra.Section3.MovingFluxEnergyComplete.movingCutoffEnergyMatrix_active {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (k : ℤ) (hk : k % 4 = 1 ∨ k % 4 = 3) (t : ℝ) (hzk : I.zetaMK m k t ≠ 0) : movingCutoffEnergyMatrix I κ m t = κ • 1 + movingCutoffEnergyTrace I κ m t • if k % 4 = 1 then Matrix.single 1 1 1 else Matrix.single 0 0 1

theorem AVenhance.Infra.Section3.MovingFluxEnergyComplete.movingFluxEnergy_active_matrix_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) (i j : Fin 2) : |(I.flux κ m t - movingCutoffEnergyMatrix I κ m t) i j| ≤ ((C₀ + C₀) / (4 * Real.pi ^ 2) * (1 / 2) + C₀ ^ 2 / (16 * Real.pi ^ 4)) * (a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κ) * (epsilon β I.Λ m ^ 2 / (κ * tau β I.Λ m))

theorem AVenhance.Infra.Section3.movingFluxEnergy_matrix_error {β C₀ : ℝ} (I : Ingredients β) (hCz : I.Czeta ≤ C₀) (hCh : I.Chat ≤ C₀) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (hκ : 0 < κ) (t : ℝ) (hcondition : epsilon β I.Λ m ^ 2 ≤ κ * tau β I.Λ m / 2) (i j : Fin 2) : |(I.flux κ m t - movingCutoffEnergyMatrix I κ m t) i j| ≤ ((C₀ + C₀) / (4 * Real.pi ^ 2) * (1 / 2) + C₀ ^ 2 / (16 * Real.pi ^ 4)) * (a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κ) * (epsilon β I.Λ m ^ 2 / (κ * tau β I.Λ m))

The full matrix flux-energy estimate, with the cutoff dependence reduced to C₀ and under the source's small-ratio condition.