OAI/Analysis/LipschitzHilbert/Estimates/TestingWeakTwo.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Recover a weak-L2 distribution bound from the restricted L1 testing inequality. Integrability supplies finiteness of the testing level set.

  1. theorem OAI.LipschitzHilbert.weak_two_of_testing line 14