OAI/Analysis/LipschitzHilbert/Trees/SourceAmplitudeEntire.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Every affine slice of the actual source amplitude is entire. All packet assignments, masks, stopping masses and boundary masses stay fixed while the complex shift parameters vary.

  1. theorem OAI.LipschitzHilbert.AngularGrid.sourcePacketAmplitude_affine_entire line 14
  2. theorem OAI.LipschitzHilbert.AngularGrid.sourcePacketAmplitude_affine_pairing_entire line 32