OAI/Analysis/LipschitzHilbert/Trees/SourceAmplitudeMeasurable.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Measurability of the actual finite source packet amplitudes. The angular cells and packet stopping levels are fixed; only the spatial weights and packet values vary. Vanishing masses are allowed.

  1. theorem OAI.LipschitzHilbert.AngularGrid.measurable_mass line 18
  2. theorem OAI.LipschitzHilbert.AngularGrid.measurable_boundaryMass line 24
  3. theorem OAI.LipschitzHilbert.AngularGrid.measurable_sourceBoundaryMass line 30
  4. theorem OAI.LipschitzHilbert.AngularGrid.measurable_sourceTransition line 37
  5. theorem OAI.LipschitzHilbert.AngularGrid.measurable_packetPathProduct line 48
  6. theorem OAI.LipschitzHilbert.AngularGrid.measurable_sourcePacketBase line 54
  7. theorem OAI.LipschitzHilbert.AngularGrid.measurable_sourcePacketAmplitude line 65
  8. theorem OAI.LipschitzHilbert.measurable_sourcePredictionValue line 83