OAI/Topology/ArtinGroups/ParabolicIntersections/MeshInsertionMatrix.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Orthogonality of weighted path insertions.

  1. theorem OAI.HarmonicArtin.ParabolicIntersections.insertion_matrix_mul_conjTranspose line 12

    Source documentation

    Rows obtained by inserting disjoint labeled detours are orthogonal.

    theorem insertion_matrix_mul_conjTranspose (f : I × P → Q)
    (hf : Function.Injective f) (a : I → ℂ) :
    let C : Matrix P Q ℂ := fun p q => ∑ i, if q=f (i,p) then a i else 0
…