OAI/MeasureTheory/Falconer/Geometry/ChartCostMeasurable.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Measurable original pair and triple costs as functions of the Gaussian rows

  1. lemma OAI.Falconer.chart_pair_cost_measurable line 13
  2. theorem OAI.Falconer.chart_triple_cost_measurable line 47