OAI/Analysis/LipschitzHilbert/Trees/SourcePositiveSelectedSynthesis.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Synthesis energy for the actual positive size-selection run. All geometric and Gram bounds are derived from the source packet data; the only analytic input here is the previously cited scalar Lepingle bound.

  1. def OAI.LipschitzHilbert.SourceLabeledLattice.selectedNearConstant line 17
  2. def OAI.LipschitzHilbert.SourceLabeledLattice.selectedFarConstant line 21
  3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.exists_positive_selected_synthesis_bound line 27