OAI/MeasureTheory/Falconer/Estimates/FarData.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Geometric data for the actual far branch

These are scale and descriptor conditions to be verified by the recursive policy. They are not additional published inputs.

  1. def OAI.Falconer.farMinimumLength line 19
  2. structure OAI.Falconer.JetStateFarData line 22
  3. def OAI.Falconer.JetStateFarData.originalMeasure line 76
  4. def OAI.Falconer.JetStateFarData.prefactor line 79
  5. def OAI.Falconer.JetStateFarData.kernel line 82
  6. def OAI.Falconer.JetStateFarData.stationaryKernel line 87
  7. def OAI.Falconer.JetStateFarData.collisionTerm line 93
  8. theorem OAI.Falconer.JetStateFarData.minimumLength_pos line 101
  9. theorem OAI.Falconer.JetStateFarData.base_one line 105
  10. theorem OAI.Falconer.JetStateFarData.prefactor_nonneg line 107
  11. theorem OAI.Falconer.JetStateFarData.list_scale_mono line 111
  12. theorem OAI.Falconer.JetStateFarData.collisionTerm_mono line 116