OAI/Analysis/LipschitzHilbert/Estimates/BoundedDuality.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Passing the interpolated simple-test pairing estimate to a bounded canonical dual test. Only finite measures and bounded functions are needed.

  1. theorem OAI.LipschitzHilbert.PhaseCombinatorics.bounded_test_of_simple_tests line 17
  2. def OAI.LipschitzHilbert.PhaseCombinatorics.canonicalDual line 57
  3. theorem OAI.LipschitzHilbert.PhaseCombinatorics.canonicalDual_measurable line 60
  4. theorem OAI.LipschitzHilbert.PhaseCombinatorics.canonicalDual_norm line 65
  5. theorem OAI.LipschitzHilbert.PhaseCombinatorics.canonicalDual_pairing line 80
  6. theorem OAI.LipschitzHilbert.PhaseCombinatorics.bounded_lp_power_le_one_of_simple_tests line 93