OAI/MeasureTheory/Falconer/Estimates/BadTripleRelation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual measurable bad-triple relation on retained original labels

  1. def OAI.Falconer.chartTripleVolume line 12
  2. lemma OAI.Falconer.chartTripleVolume_measurable line 16
  3. def OAI.Falconer.badChartTriples line 31
  4. lemma OAI.Falconer.badChartTriples_measurable line 36
  5. lemma OAI.Falconer.badChartTriples_retained line 51