OAI/Analysis/LipschitzHilbert/Trees/SourceTypeUniformCentral.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The numerical thresholds are chosen before all spatial and coefficient index types. These are the existing source estimates with their universal type binders moved inside the eventual statement; no bound changes.

  1. theorem OAI.LipschitzHilbert.AngularGrid.eventually_source_central_sum_gain_types line 15
  2. theorem OAI.LipschitzHilbert.AngularGrid.eventually_source_central_from_paths_types line 100