OAI/Analysis/LipschitzHilbert/Estimates/RestrictedStrongForm.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The restricted-to-strong estimate for the actual finite amplitude approximations of Hilbert-valued functions.

  1. def OAI.LipschitzHilbert.amplitudePiece line 16
  2. def OAI.LipschitzHilbert.amplitudeApprox line 19
  3. theorem OAI.LipschitzHilbert.amplitudePiece_measurable line 22
  4. theorem OAI.LipschitzHilbert.amplitudePiece_bounded line 27
  5. theorem OAI.LipschitzHilbert.amplitudePiece_supported line 38
  6. theorem OAI.LipschitzHilbert.amplitudeApprox_bilinear line 43
  7. theorem OAI.LipschitzHilbert.restricted_strong_finite_amplitudes line 57