OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousCanonicalLogEstimates.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Robin and derivative-row estimates for the canonical outgoing columns

Both estimates follow from the already constructed all-order expansions. The physical powers cancel between the value matrix and its inverse.

  1. theorem OAI.DefocusingNLS.homogeneous_canonical_outgoing_log_estimates line 18