OAI/Analysis/PureInfiniteness/StateCutMass.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Quantitative preservation of state mass under the spectral cut used in the product-state excision argument.

  1. theorem OAI.WeakPureInfiniteness.state_square_cut_pos line 16