OAI/Analysis/KadisonKastler/RealThresholdSelection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Selecting a spectral threshold in the unit interval

The finite spectral cut functions vanish outside [-1,1]. Their global energy estimates therefore apply to a finite measure of total mass two.

  1. theorem OAI.KadisonKastler.exists_good_real_threshold line 18