Iterates Matrix Integral Sum

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_matrix_pairing_transpose (a b : Homogenization.Vec 2) (Q : Matrix (Fin 2) (Fin 2) ℝ) : Homogenization.vecDot a (Q.transpose.mulVec b) = Homogenization.vecDot b (Q.mulVec a)

Exact transpose reversal of a scalar matrix pairing.

theorem AVenhance.Infra.Section4.iterate_unitCube_integrable_of_continuous {f : Homogenization.Vec 2 → ℝ} (hf : Continuous f) : MeasureTheory.IntegrableOn f unitCube MeasureTheory.volume

Continuous fields on the actual compact torus cell are integrable.

theorem AVenhance.Infra.Section4.iterate_matrix_pairing_integral_eq_sum {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {a b : X → Homogenization.Vec 2} {Q : X → Matrix (Fin 2) (Fin 2) ℝ} (hi : ∀ (j k : Fin 2), MeasureTheory.Integrable (fun (z : X) => Q z j k * a z j * b z k) μ) : ∫ (z : X), Homogenization.vecDot (a z) ((Q z).mulVec (b z)) ∂μ = ∑ j : Fin 2, ∑ k : Fin 2, ∫ (z : X), Q z j k * a z j * b z k ∂μ

Finite matrix pairings commute with integration under componentwise integrability; coefficients retain their original order.