OAI/Analysis/LipschitzHilbert/ConditionalMain.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Theorem 1.1 of the supplied manuscript, conditional on the four precisely cited published inputs. The principal value is the actual pointwise symmetric limit on Schwartz functions.

  1. def OAI.LipschitzHilbert.ShortHilbertConclusion line 15

    Also declared: ComparatorChallenges/LipschitzHilbert.lean:44 (same declaration text).

  2. theorem OAI.LipschitzHilbert.conditional_main line 32