MatrixView
plain-language theorem explainer
MatrixView wraps an arbitrary complex matrix A as the concrete data for a transfer kernel over a finite index set ι. Researchers constructing stochastic operators or bridging explicit matrices to continuous linear maps in the YM module cite this structure. The declaration is a direct structure with one field and no proof obligations or constraints on entries.
Claim. Let ι be a finite type with decidable equality. A MatrixView on ι is a structure containing a single field A : ι × ι → ℂ.
background
In the YM.Kernel module, transfer kernels are realized as continuous linear maps on ℂ-valued functions over finite sets. MatrixView supplies the underlying matrix data that downstream constructions convert via Matrix.toLin' and CLM.ofLM. The module imports Mathlib for matrix and linear-map infrastructure while depending on the constant A (active edge count per tick) from IntegrationGap, Masses.Anchor, and Modal.Actualization.
proof idea
Direct structure definition introducing the field A of type Matrix ι ι ℂ. No lemmas, tactics, or reductions are applied.
why it matters
MatrixView supplies the matrix input required by buildKernelFromMatrix, constantStochastic3x3, KernelHasMatrixView, and MatrixBridge. These objects realize the intertwining condition K.T = CLM.ofLM (Matrix.toLin' V.A) that connects explicit matrices to abstract kernels. The wrapper supports explicit 3×3 stochastic constructions used in the Recognition Science treatment of transfer operators at D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.