OAI/Geometry/CAT0Fillings/Differentiation/ErrorModulus.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CAT0Fillings.MetricDifferentiation.measurable_metricSeminorm_apply line 23
  2. def OAI.CAT0Fillings.MetricDifferentiation.metricErrorTerm line 28
  3. def OAI.CAT0Fillings.MetricDifferentiation.metricErrorModulus line 33
  4. lemma OAI.CAT0Fillings.MetricDifferentiation.metricErrorTerm_nonneg line 37
  5. lemma OAI.CAT0Fillings.MetricDifferentiation.metricErrorTerm_le line 45
  6. lemma OAI.CAT0Fillings.MetricDifferentiation.bddAbove_metricErrorTerm line 60
  7. lemma OAI.CAT0Fillings.MetricDifferentiation.metricErrorModulus_nonneg line 65
  8. lemma OAI.CAT0Fillings.MetricDifferentiation.metricErrorModulus_le line 70
  9. lemma OAI.CAT0Fillings.MetricDifferentiation.measurable_metricErrorModulus line 74
  10. lemma OAI.CAT0Fillings.MetricDifferentiation.metricErrorModulus_le_of_bound line 87
  11. lemma OAI.CAT0Fillings.MetricDifferentiation.metricErrorModulus_tendsto_zero line 99
  12. lemma OAI.CAT0Fillings.MetricDifferentiation.metricErrorModulus_bound line 130