OAI/Analysis/LipschitzHilbert/Estimates/FiniteSignedFunctions.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Finite randomization for actual measurable functions. Membership in L2 is recovered from signed sums and is not assumed in advance.

  1. def OAI.LipschitzHilbert.signedFunction line 15
  2. theorem OAI.LipschitzHilbert.signedFunction_isolate line 19
  3. theorem OAI.LipschitzHilbert.memLp_of_signedFunction line 32
  4. theorem OAI.LipschitzHilbert.signedLpTerm_coe line 39
  5. theorem OAI.LipschitzHilbert.signedFunction_toLp line 50
  6. theorem OAI.LipschitzHilbert.signedFunction_square_bound line 63