OAI/Analysis/LipschitzHilbert/Trees/SourceAmplitudeExponential.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual source packet path is a single exponential of the sum of its logarithmic transition ratios. This exact formula is used to integrate an affine phase slice on sets where those finitely many logs are bounded.

  1. def OAI.LipschitzHilbert.AngularGrid.pathLogCombination line 15
  2. theorem OAI.LipschitzHilbert.AngularGrid.packetPathProduct_affine_exp line 21
  3. theorem OAI.LipschitzHilbert.AngularGrid.sourcePacketAmplitude_affine_exp line 36