OAI/Analysis/LipschitzHilbert/Trees/SourceAmplitudeBounds.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

On each fixed exhaustion the original source amplitude is bounded for every complex phase. Nonnegative real phases give the sharper phase-independent bound needed on the simplex tube.

  1. theorem OAI.LipschitzHilbert.AngularGrid.sourcePacketAmplitude_norm_on_exhaustion line 15
  2. theorem OAI.LipschitzHilbert.AngularGrid.sourcePacketAmplitude_norm_le_radius line 50