OAI/Analysis/LipschitzHilbert/Trees/SourceAmplitudeExhaustion.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A single exhaustion, independent of the complex phase, bounds all original packet bases and the absolute logarithms along their paths.

  1. def OAI.LipschitzHilbert.AngularGrid.pathLogSize line 15
  2. theorem OAI.LipschitzHilbert.AngularGrid.pathLogSize_nonneg line 21
  3. theorem OAI.LipschitzHilbert.AngularGrid.pathLogCombination_norm_le line 26
  4. def OAI.LipschitzHilbert.AngularGrid.sourceAmplitudeRadius line 46
  5. theorem OAI.LipschitzHilbert.AngularGrid.measurable_sourceAmplitudeRadius line 56
  6. theorem OAI.LipschitzHilbert.AngularGrid.sourceAmplitudeRadius_base_le line 74
  7. theorem OAI.LipschitzHilbert.AngularGrid.sourceAmplitudeRadius_log_le line 92
  8. theorem OAI.LipschitzHilbert.AngularGrid.sourcePacketAmplitude_integral_entire_on_exhaustion line 112