Iterates Matrix Primitive Assembly #
Support for the Armstrong–Vicol anomalous-diffusion formalization.
theorem
AVenhance.Infra.Section4.iterate_matrix_primitive_component_assembly
{X : Type u_1}
{Y : Type u_2}
[MeasurableSpace X]
[MeasurableSpace Y]
{μ : MeasureTheory.Measure X}
{ν : MeasureTheory.Measure Y}
{a b ma mb : X → Homogenization.Vec 2}
{C Q : X → Matrix (Fin 2) (Fin 2) ℝ}
{as bs : Y → Homogenization.Vec 2}
{Qs : Y → Matrix (Fin 2) (Fin 2) ℝ}
(hc : ∀ (j k : Fin 2), MeasureTheory.Integrable (fun (z : X) => C z j k * a z j * b z k) μ)
(hbd : ∀ (j k : Fin 2), MeasureTheory.Integrable (fun (x : Y) => Qs x j k * as x j * bs x k) ν)
(hp : ∀ (j k : Fin 2), MeasureTheory.Integrable (fun (z : X) => Q z j k * a z j * mb z k) μ)
(hu : ∀ (j k : Fin 2), MeasureTheory.Integrable (fun (z : X) => Q z j k * ma z j * b z k) μ)
(hcomponent :
∀ (j k : Fin 2),
∫ (z : X), C z j k * a z j * b z k ∂μ = ∫ (x : Y), Qs x j k * as x j * bs x k ∂ν - ∫ (z : X), Q z j k * a z j * mb z k ∂μ - ∫ (z : X), Q z j k * ma z j * b z k ∂μ)
:
Finite-dimensional assembly of independently proved component primitive identities. This lemma performs only linearity of integrals and finite sums.