OAI/Analysis/LipschitzHilbert/Trees/SourceLabeledErrorBudget.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Fixed profile order, geometric bounds, and selector multiplicity give polynomial source constants without a factor counting the available labels.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.eventually_absoluteConstant_le line 16
  2. theorem OAI.LipschitzHilbert.LabeledAngularErrorFamily.eventually_sourceAmplitude_le line 44