OAI/Topology/ArtinGroups/ParabolicIntersections/MeshGraphNilpotence.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Finite mesh path bounds, including disconnected positive Cartan graphs.

  1. theorem OAI.HarmonicArtin.ParabolicIntersections.connected_mesh_paths_vanish line 12
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.meshPathEvaluate_longer line 26
  3. def OAI.HarmonicArtin.ParabolicIntersections.meshPathInComponent line 39
  4. lemma OAI.HarmonicArtin.ParabolicIntersections.meshPathInComponent_evaluate line 47
  5. lemma OAI.HarmonicArtin.ParabolicIntersections.mesh_component_cartan line 60
  6. def OAI.HarmonicArtin.ParabolicIntersections.meshComponentNeighborEquiv line 77
  7. theorem OAI.HarmonicArtin.ParabolicIntersections.positive_cartan_mesh_paths_vanish line 86

    Source documentation

    Every finite graph with positive definite Cartan form has a finite all-plus mesh path bound, whether or not the graph is connected.

    theorem positive_cartan_mesh_paths_vanish
    (hcartan : ((2 : ℝ) • (1 : Matrix V V ℝ)-G.adjMatrix ℝ).PosDef)
    (B : ∀ u v, G.Adj u v → R)
    (hmesh : ∀ v, (∑ u : {u : V // G.Adj u v},
      B v u.val u.property.symm * B u.val v u.property)=0) :
    ∃ N : ℕ, 0<N ∧ ∀ v p, meshPathEvaluate G B N v p=0 := by
…

    Mentions: OAI.HarmonicArtin.ParabolicIntersections.meshPathEvaluate