OAI/MeasureTheory/Falconer/Angular/AngularEnvelope.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

A bounded supremum of the actual admissible endpoint energies

The admissible class records only the existing chart-symbol control and the required support. Its envelope is the real supremum of the original endpoint-transform energies, with zero inserted to ensure nonemptiness.

  1. def OAI.Falconer.AngularAdmissible line 19
  2. theorem OAI.Falconer.AngularAdmissible.spatialMultiplier line 24
  3. theorem OAI.Falconer.AngularAdmissible.spatialFourier line 31
  4. theorem OAI.Falconer.AngularAdmissible.conj line 39
  5. def OAI.Falconer.angularEnergyValues line 51
  6. def OAI.Falconer.angularEnvelope line 59
  7. def OAI.Falconer.angularEnvelopeBound line 64
  8. theorem OAI.Falconer.angularEnergyValues_nonempty line 70
  9. theorem OAI.Falconer.angularEnergyValues_bound line 76
  10. theorem OAI.Falconer.angularEnergyValues_bddAbove line 94
  11. theorem OAI.Falconer.angularEnvelope_nonneg line 103
  12. theorem OAI.Falconer.angularEnvelope_le_bound line 111
  13. theorem OAI.Falconer.admissible_energy_le_angularEnvelope line 121
  14. theorem OAI.Falconer.spatial_endpoint_energy_le_envelope line 135
  15. theorem OAI.Falconer.AngularAdmissible.mono line 159
  16. theorem OAI.Falconer.angularEnvelope_mono line 169