OAI/Analysis/LipschitzHilbert/Trees/SourceSelectedEnvelopeEnergy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The short-envelope estimate for an actual positive size-selection run, with the spatial and angular widths kept independent.

  1. def OAI.LipschitzHilbert.SourceLabeledLattice.SizeStoppingRun.selectedEnvelopePackingConstant line 21
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.SizeStoppingRun.selected_short_envelope_energy line 24