OAI/Analysis/LipschitzHilbert/Trees/SourcePhysicalAmplitudeMeasurable.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The masked physical packet family is measurable in the spatial point. Its analyzing coefficients are fixed integrals; no continuity of the direction selector is required.

  1. theorem OAI.LipschitzHilbert.vectorPacketSynthesis_joint_continuous line 16
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.rawBand_slope_continuous line 32
  3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.masked_rawBand_continuous line 49
  4. theorem OAI.LipschitzHilbert.AngularGrid.source_masked_amplitude_measurable line 63