OAI/MeasureTheory/Falconer/Estimates/FarEnvelope.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The far reduction for the full recursive symbol supremum

  1. def OAI.Falconer.JetStateFarData.envelope line 15
  2. theorem OAI.Falconer.JetStateFarData.envelope_le_of_energy_le line 21
  3. def OAI.Falconer.JetStateFarData.farError line 37
  4. theorem OAI.Falconer.exists_far_envelope_step line 44
  5. def OAI.Falconer.PolicyJetData.envelope line 67
  6. theorem OAI.Falconer.PolicyJetData.farData_envelope line 73