OAI/Geometry/PrescribedRicci/UniformCoefficientOscillation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform Coefficient Oscillation.

  1. lemma OAI.MongeAmpere.matrix_trace_norm_le line 21
  2. lemma OAI.MongeAmpere.inverse_difference_bound line 26
  3. lemma OAI.EllipticKernel.traceBilin_difference_bound line 47
  4. theorem OAI.Anticanonical.SourceSmooth.KaehlerMetric.volumePath_metric_lipschitz_on_compact line 62