OAI/Analysis/LipschitzHilbert/Trees/SourceStoppedMassPower.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The phase power of every active stopped mass is bounded by the same subexponential factor. This uses the mass at the initial node, rather than a separate bound at every generation.

  1. theorem OAI.LipschitzHilbert.mass_power_le_exp_sqrt line 13
  2. theorem OAI.LipschitzHilbert.stopped_mass_power_le_exp_sqrt line 34