OAI/MeasureTheory/Falconer/Graphs/GraphChartVariation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PlanarFalconer.quarterTurn_sub line 9

    Distinct definitions of this name: OAI/MeasureTheory/Falconer/Angular/ActualAngularTests.lean:94 (different declaration text). Qualify references as OAI.PlanarFalconer.quarterTurn_sub@path.

  2. theorem OAI.PlanarFalconer.graphChartZ_dist_le line 14
  3. def OAI.PlanarFalconer.graphChartAxis line 43
  4. theorem OAI.PlanarFalconer.graphChartAxis_dist_le line 45
  5. theorem OAI.PlanarFalconer.graph_sign_bin_pair_variation line 57
  6. theorem OAI.PlanarFalconer.graph_complete_support_representative line 77