OAI/Analysis/SphereIsometry/BarycentricMesh.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The mesh estimate for barycentric subdivision

The larger face is split into the smaller face and its complement. Its barycenter is the corresponding weighted average, giving the exact factor 1 - S.card / T.card. A dimension bound gives the uniform contraction.

  1. theorem OAI.Tingley.norm_finiteBarycenter_sub_le_of_subsets line 29
  2. theorem OAI.Tingley.finiteBarycenter_partition line 42
  3. theorem OAI.Tingley.norm_finiteBarycenter_sub_le_card line 70
  4. theorem OAI.Tingley.norm_finiteBarycenter_sub_le_mesh line 114
  5. theorem OAI.Tingley.norm_finiteBarycenter_sub_le_of_comparable line 143