OAI/Topology/ArtinGroups/ParabolicIntersections/MeshContraction.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The path-space loop identity and extension functor.

  1. theorem OAI.HarmonicArtin.ParabolicIntersections.meshContraction_loop line 13

    Source documentation

    Inserting and then contracting a final backtrack multiplies by the Perron eigenvalue. This is proved for the actual path matrices.

    theorem meshContraction_loop (μ : V → ℝ) (hμ : ∀ v, 0<μ v) (δ : ℝ)
    (heigen : ∀ v, (∑ u : {u : V // G.Adj u v}, μ u)=δ*μ v)
    (n : ℕ) (v : V) :
    meshContractionMatrix G μ n v * (meshContractionMatrix G μ n v).conjTranspose =
      (δ : ℂ) • (1 : Matrix (MeshPaths G n v) (MeshPaths G n v) ℂ) := by
…

    Mentions: OAI.HarmonicArtin.ParabolicIntersections.meshContractionMatrix, OAI.HarmonicArtin.ParabolicIntersections.MeshPaths

  2. lemma OAI.HarmonicArtin.ParabolicIntersections.meshExtend_one line 35
  3. lemma OAI.HarmonicArtin.ParabolicIntersections.meshExtend_mul line 48
  4. lemma OAI.HarmonicArtin.ParabolicIntersections.meshExtend_adjoint line 55
  5. lemma OAI.HarmonicArtin.ParabolicIntersections.meshExtend_sub line 61
  6. lemma OAI.HarmonicArtin.ParabolicIntersections.meshExtend_smul line 67