OAI/Topology/ArtinGroups/ParabolicIntersections/MeshGraphWeights.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Positive mesh weights for a connected graph with positive Cartan form.

  1. lemma OAI.HarmonicArtin.ParabolicIntersections.mesh_adjacency_sum line 11
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.mesh_connected_eigenvector_pos line 16
  3. theorem OAI.HarmonicArtin.ParabolicIntersections.mesh_graph_positive_weights line 40

    Source documentation

    Positive definiteness of 2I-B gives exactly the spectral interval needed by the essential-path argument, on each nontrivial component.

    theorem mesh_graph_positive_weights (hG : G.Connected)
    (hedge : ∃ u v, G.Adj u v)
    (hcartan : ((2 : ℝ) • (1 : Matrix V V ℝ)-G.adjMatrix ℝ).PosDef) :
    ∃ (μ : V → ℝ) (d : ℝ), (∀ v, 0<μ v) ∧ 0<d ∧ d<2 ∧
      ∀ v, (∑ u : {u : V // G.Adj u v}, μ u)=d*μ v := by
…