OAI/Analysis/LipschitzHilbert/Trees/SourceMovingException.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The moving good-path exceptional set is charged to the original sum. Its exp(-9L) area beats every fixed polynomial L2 loss.

  1. theorem OAI.LipschitzHilbert.eventually_original_moving_exception line 14