OAI/Analysis/LipschitzHilbert/Trees/SourceAmplitudeIntegral.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The integrated affine slices of the original source packet amplitude are entire on bounded logarithmic-coefficient exhaustions.

  1. def OAI.LipschitzHilbert.AngularGrid.sourcePathLog line 16
  2. theorem OAI.LipschitzHilbert.AngularGrid.measurable_sourcePathLog line 23
  3. theorem OAI.LipschitzHilbert.AngularGrid.sourcePacketAmplitude_integral_affine_entire_on line 34