MeshPathSpaces.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual finite path spaces and weighted last-backtrack contractions.

def OAI.HarmonicArtin.ParabolicIntersections.MeshPaths line 12
Source documentation
Paths of length n, indexed by their final vertex. The recursive presentation makes extension of prefix operators a block-diagonal map.
```
def MeshPaths : ℕ → V → Type
  | 0, _ => PUnit
  | n+1, v => Σ u : {u : V // G.Adj u v}, MeshPaths n u.val
```
instance OAI.HarmonicArtin.ParabolicIntersections.meshPathsFintype line 16
def OAI.HarmonicArtin.ParabolicIntersections.meshInsertBacktrack line 25
Source documentation
Attach the last two edges v,u,v to a path ending at v.
```
def meshInsertBacktrack {n : ℕ} {v : V} (u : {u : V // G.Adj u v})
    (p : MeshPaths G n v) : MeshPaths G (n+2) v :=
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.MeshPaths
lemma OAI.HarmonicArtin.ParabolicIntersections.meshInsertBacktrack_injective line 29
def OAI.HarmonicArtin.ParabolicIntersections.meshContractionMatrix line 44
Source documentation
The contraction coefficient is the positive square root used in the essential-path representation of the mesh algebra.
```
noncomputable def meshContractionMatrix (μ : V → ℝ) (n : ℕ) (v : V) :
    Matrix (MeshPaths G n v) (MeshPaths G (n+2) v) ℂ :=
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.MeshPaths
def OAI.HarmonicArtin.ParabolicIntersections.meshExtendMatrix line 50
Source documentation
Extending a prefix operator by one edge, without changing that edge.
```
noncomputable def meshExtendMatrix {m n : ℕ}
    (T : ∀ v, Matrix (MeshPaths G m v) (MeshPaths G n v) ℂ) (v : V) :
    Matrix (MeshPaths G (m+1) v) (MeshPaths G (n+1) v) ℂ :=
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.MeshPaths