OAI/Topology/ArtinGroups/ParabolicIntersections/MeshPathEvaluation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.ParabolicIntersections.meshPathEvaluate line 12
2. lemma OAI.HarmonicArtin.ParabolicIntersections.meshPathEvaluate_insert line 18
3. lemma OAI.HarmonicArtin.ParabolicIntersections.meshApply_contraction_adjoint line 23
4. lemma OAI.HarmonicArtin.ParabolicIntersections.meshPathEvaluate_contracts line 35
5. lemma OAI.HarmonicArtin.ParabolicIntersections.meshPathEvaluate_extend line 54
6. theorem OAI.HarmonicArtin.ParabolicIntersections.meshPathEvaluate_projection line 72

   Source documentation

   Every recursively defined projection acts as the identity after evaluation in an algebra satisfying the weighted mesh relations.

   theorem meshPathEvaluate_projection (μ : V → ℝ) (δ : ℝ)
       (B : ∀ u v, G.Adj u v → R)
       (hmesh : ∀ v, (∑ u : {u : V // G.Adj u v},
         (Real.sqrt (μ u/μ v) : ℂ) • (B v u.val u.property.symm * B u.val v u.property))=0) :
       ∀ n v, meshApply (meshProjection G μ δ n v) (meshPathEvaluate G B n v)=
         meshPathEvaluate G B n v := by
   …

   Mentions: OAI.HarmonicArtin.ParabolicIntersections.meshApply, OAI.HarmonicArtin.ParabolicIntersections.meshProjection, OAI.HarmonicArtin.ParabolicIntersections.meshPathEvaluate

7. theorem OAI.HarmonicArtin.ParabolicIntersections.weighted_mesh_paths_vanish line 99

   Source documentation

   A single finite path length vanishes in every algebra satisfying the weighted mesh relations. The proof uses the actual finite path matrices.

   theorem weighted_mesh_paths_vanish (μ : V → ℝ) (hμ : ∀ v, 0<μ v)
       (δ : ℝ) (hδ0 : 0<δ) (hδ2 : δ<2)
       (heigen : ∀ v, (∑ u : {u : V // G.Adj u v}, μ u)=δ*μ v)
       (B : ∀ u v, G.Adj u v → R)
       (hmesh : ∀ v, (∑ u : {u : V // G.Adj u v},
         (Real.sqrt (μ 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