MeshTrace.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Positive weighted traces detect vanishing of all endpoint projections.

def OAI.HarmonicArtin.ParabolicIntersections.meshWeightedTrace line 12
lemma OAI.HarmonicArtin.ParabolicIntersections.meshWeightedTrace_nonneg line 16
theorem OAI.HarmonicArtin.ParabolicIntersections.meshWeightedTrace_zero line 27
Source documentation
Strict positivity of the vertex weights turns a zero weighted trace of orthogonal projections into the vanishing of each projection.
```
theorem meshWeightedTrace_zero {D : V → Type} [∀ v, Fintype (D v)]
    (μ : V → ℝ) (hμ : ∀ v, 0<μ v) (P : ∀ v, Matrix (D v) (D v) ℂ)
    (hstar : ∀ v, (P v).conjTranspose=P v) (hsq : ∀ v, P v*P v=P v)
    (hz : meshWeightedTrace μ P=0) : ∀ v, P v=0 := by
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.meshWeightedTrace
lemma OAI.HarmonicArtin.ParabolicIntersections.meshExtend_trace line 54
def OAI.HarmonicArtin.ParabolicIntersections.meshEdgeFlip line 61
Source documentation
Reversal of an oriented edge exchanges the two endpoint sums.
```
def meshEdgeFlip : (Σ v : V, {u : V // G.Adj u v}) ≃
    (Σ v : V, {u : V // G.Adj u v}) where
…
```
lemma OAI.HarmonicArtin.ParabolicIntersections.meshWeightedTrace_extend line 69
Source documentation
Extension multiplies the weighted trace by the Perron eigenvalue.
```
lemma meshWeightedTrace_extend (μ : V → ℝ) (δ : ℝ)
    (heigen : ∀ v, (∑ u : {u : V // G.Adj u v}, μ u)=δ*μ v)
    {n : ℕ} (P : ∀ v, Matrix (MeshPaths G n v) (MeshPaths G n v) ℂ) :
    meshWeightedTrace μ (meshExtendMatrix G P)=
      (δ : ℂ)*meshWeightedTrace μ P := by
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.MeshPaths, OAI.HarmonicArtin.ParabolicIntersections.meshWeightedTrace, OAI.HarmonicArtin.ParabolicIntersections.meshExtendMatrix