OAI/Analysis/LipschitzHilbert/Estimates/FiniteRestrictedStrong.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The finite-amplitude restricted-to-strong estimate from Section 2. The matrix entries are the restricted bilinear pairings.

  1. def OAI.LipschitzHilbert.restrictedStrongConstant line 12
  2. theorem OAI.LipschitzHilbert.restrictedStrongConstant_pos line 15
  3. theorem OAI.LipschitzHilbert.finite_restricted_strong line 21