OAI/Analysis/LipschitzHilbert/Phase/SourceTypeUniformInterpolation.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_diagonal_finite_phases_types line 15
  2. theorem OAI.LipschitzHilbert.AngularGrid.eventually_source_root_diagonal_from_paths_types line 101