OAI/Analysis/LipschitzHilbert/Estimates/ConditionalUniformTruncation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The uniform sharp-truncation estimate at reciprocal Lipschitz scale. The explicit radius is deliberately smaller than the allowed absolute radius; the operator constant is independent of both cutoffs and the field.

  1. theorem OAI.LipschitzHilbert.conditional_uniform_truncation line 15