OAI/Geometry/PrescribedRicci/PathUniformSobolevBase.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Path Uniform Sobolev Base.

  1. structure OAI.Anticanonical.SourceSmooth.KaehlerMetric.NormalizedPathSolution line 27
  2. lemma OAI.Anticanonical.SourceSmooth.KaehlerMetric.volumePath_background_laplacian_bound line 37
  3. lemma OAI.GlobalElliptic.Localizers.uniform_zero_of_bound line 69
  4. theorem OAI.GlobalElliptic.GluingData.volumePath_uniform_H2 line 89