OAI/Geometry/PrescribedPotential/MetricLocalization.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Metric Localization.

  1. lemma OAI.MetricLocalization.contDiffOn_matrix_det line 20
  2. lemma OAI.MetricLocalization.contDiffOn_matrix_adjugate line 31
  3. lemma OAI.MetricLocalization.contDiffOn_matrix_inv line 51
  4. lemma OAI.MetricLocalization.trace_coefficient_smooth line 57
  5. lemma OAI.MetricLocalization.smooth_bump_smul line 79
  6. lemma OAI.MetricLocalization.small_smooth_extension line 92
  7. theorem OAI.MetricLocalization.local_coefficient_extension line 136
  8. theorem OAI.Anticanonical.SourceSmooth.KaehlerMetric.local_inverse_coefficients line 202