OAI/Analysis/LipschitzHilbert/Trees/SourceTypeUniformMoments.lean

GitHub source file

3 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.eventually_source_crude_mass_budget_types line 14
  2. theorem OAI.LipschitzHilbert.eventually_source_damped_vertex_root_types line 67
  3. theorem OAI.LipschitzHilbert.AngularGrid.eventually_source_tree_vertex_moment_types line 89