OAI/Geometry/PrescribedPotential/HigherMetricOperator.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Higher Metric Operator.

  1. lemma OAI.MetricLocalization.differential_cutoff_bound_integer line 21
  2. lemma OAI.GlobalElliptic.GluingData.complexL_piece_bound_integer line 54
  3. lemma OAI.GlobalElliptic.GluingData.complexL_bound_integer line 68
  4. def OAI.GlobalElliptic.GluingData.completedLOrder line 75
  5. lemma OAI.GlobalElliptic.GluingData.completedLOrder_embed line 78
  6. lemma OAI.GlobalElliptic.GluingData.completedLOrder_lower line 82