OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/StableGraphApplication.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Direct application of the stable graph to endpoint remainders

Only the concrete projected block and pointwise remainder estimates occur as hypotheses. The weighted sources and the fixed sequence are constructed inside the proof, and the conclusion is the original endpoint recurrence.

  1. theorem OAI.DefocusingNLS.exists_stableGraph_actual_endpoint_sequence line 20