OAI/Analysis/LipschitzHilbert/Packets/SourceSupportedWeightedDerivative.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The weighted derivative estimate uses upper scale bounds only at actual packet items. Empty scales do not constrain the top window.

  1. theorem OAI.LipschitzHilbert.top_weighted_selected_derivative_of_supported line 10
  2. theorem OAI.LipschitzHilbert.top_weighted_selected_derivative_bounded_of_supported line 45