OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousCompactLocalEstimate.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The local physical observation form of a compact Y error

A failure of the estimate produces unit vectors with vanishing observation on expanding balls. Their weak subsequential limit is zero by faithfulness of the physical realization, contradicting the proved compact-error bound.

  1. theorem OAI.DefocusingNLS.homogeneousCompactOperator_local_estimate line 20