OAI/Analysis/LipschitzHilbert/Trees/SourceTotalWeightBudget.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The two different mass budgets used in the assembly: integrating the top count on the testing set costs N|F|, whereas integrating all weights on the plane costs N²|F|. Their polynomial losses are explicit.

  1. theorem OAI.LipschitzHilbert.source_testing_weight_integral line 16
  2. theorem OAI.LipschitzHilbert.eventually_source_global_weight_integral line 37