English
Applying comp to a diagonal matrix built from a diagonal of diagonal blocks yields the corresponding diagonal of the two-level diagonal of d.
Русский
Применение компоновки к диагональной матрице, составленной из диагоналей диагональных блоков, даёт соответствующую диагональ из двухуровневой диагональной матрицы d.
LaTeX
$$$ \mathrm{comp}(I,I,J,J,R)\left(\mathrm{diagonal}(\lambda i.\ \mathrm{diagonal}(\lambda j. d(i,j)))) = \mathrm{diagonal}(\lambda ij. d(i,j)) $$$
Lean4
@[simp]
theorem comp_diagonal_diagonal [DecidableEq I] [DecidableEq J] [Zero R] (d : I → J → R) :
comp I I J J R (diagonal fun i => diagonal fun j => d i j) = diagonal fun ij => d ij.1 ij.2 :=
by
ext ⟨i₁, j₁⟩ ⟨i₂, j₂⟩
dsimp [comp_apply]
obtain hi | rfl := ne_or_eq i₁ i₂
· rw [diagonal_apply_ne _ hi, diagonal_apply_ne _ (ne_of_apply_ne Prod.fst hi), Matrix.zero_apply]
rw [diagonal_apply_eq]
obtain hj | rfl := ne_or_eq j₁ j₂
· rw [diagonal_apply_ne _ hj, diagonal_apply_ne _ (ne_of_apply_ne Prod.snd hj)]
rw [diagonal_apply_eq, diagonal_apply_eq]
