OAI/Geometry/NodalSets/Coefficients/SupportedCoefficientChartBounds.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Yau.Target.roundTensorPerturbation_any_entry line 14
  2. lemma OAI.Yau.Target.round_increment_any_entry_smooth line 24
  3. lemma OAI.Yau.Target.intrinsic_any_increment_pullback_smooth line 32
  4. theorem OAI.Yau.Target.supported_sphere_coefficient_coord_bound line 44
  5. theorem OAI.Yau.Target.supported_sphere_coefficient_bound line 85