OAI/Analysis/LipschitzHilbert/Phase/AngularAnalyticWeight.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Analytic transition weights for the shared angular packet family. The exact modulus is the child-to-boundary mass ratio raised to the real part of the corresponding complex parameter.

  1. def OAI.LipschitzHilbert.AngularGrid.analyticTransition line 15
  2. theorem OAI.LipschitzHilbert.AngularGrid.analyticTransition_norm line 19
  3. theorem OAI.LipschitzHilbert.AngularGrid.analyticTransition_norm_le_one line 28
  4. theorem OAI.LipschitzHilbert.AngularGrid.analyticTransition_entire line 35
  5. theorem OAI.LipschitzHilbert.AngularGrid.packetPathProduct_norm line 40