OAI/Analysis/CircleDomains/Topology/SphereChartSmallSets.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Quantitative finite-chart Lipschitz constants on small convex sets.

  1. theorem OAI.CircleDomainRigidity.quadratic_weight_compare line 16
  2. theorem OAI.CircleDomainRigidity.decay_weight_compare line 25
  3. theorem OAI.CircleDomainRigidity.finite_sphere_chart_lipschitz_on_small_convex line 32