OAI/Topology/ArtinGroups/ParabolicIntersections/MeshNormalization.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Passage from the weighted essential-path relations to all-plus meshes.

  1. lemma OAI.HarmonicArtin.ParabolicIntersections.mesh_normalization_weight line 10
  2. def OAI.HarmonicArtin.ParabolicIntersections.meshRescale line 19
  3. lemma OAI.HarmonicArtin.ParabolicIntersections.meshRescale_relation line 23
  4. def OAI.HarmonicArtin.ParabolicIntersections.meshPathScale line 40
  5. lemma OAI.HarmonicArtin.ParabolicIntersections.meshPathScale_ne_zero line 46
  6. lemma OAI.HarmonicArtin.ParabolicIntersections.meshRescale_evaluate line 58
  7. theorem OAI.HarmonicArtin.ParabolicIntersections.allPlus_mesh_paths_vanish line 73

    Source documentation

    Unweighted all-plus mesh relations suffice for the same finite path bound. The rescaling factors are explicitly proved nonzero.

    theorem allPlus_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},
      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