OAI/Topology/ArtinGroups/ParabolicIntersections/MeshAdjacent.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Adjacent contraction identities on the actual finite path spaces.

  1. lemma OAI.HarmonicArtin.ParabolicIntersections.meshContraction_mul line 10
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.meshContraction_head line 21
  3. lemma OAI.HarmonicArtin.ParabolicIntersections.meshContraction_return line 45
  4. lemma OAI.HarmonicArtin.ParabolicIntersections.mesh_sqrt_reciprocal line 53
  5. theorem OAI.HarmonicArtin.ParabolicIntersections.meshContraction_adjacent line 62

    Source documentation

    Contracting after insertion at the preceding position is the identity. The two weights are reciprocal positive square roots.

    theorem meshContraction_adjacent (μ : V → ℝ) (hμ : ∀ v, 0<μ v)
    (n : ℕ) (v : V) :
    meshContractionMatrix G μ (n+1) v *
      meshExtendMatrix G (fun u => (meshContractionMatrix G μ n u).conjTranspose) v =
      (1 : Matrix (MeshPaths G (n+1) v) (MeshPaths G (n+1) v) ℂ) := by
…

    Mentions: OAI.HarmonicArtin.ParabolicIntersections.meshContractionMatrix, OAI.HarmonicArtin.ParabolicIntersections.meshExtendMatrix, OAI.HarmonicArtin.ParabolicIntersections.MeshPaths