OAI/Analysis/ModularRecovery/
726 declarations, 0 contain sorry, 0 declared as axioms; 27 files
Files
- CanonicalCalculus.lean 50 declarations
- CanonicalGraph.lean 42 declarations
- CanonicalPolar.lean 32 declarations
- CanonicalTomita.lean 30 declarations
- Centralizer.lean 12 declarations
- Commutant.lean 12 declarations
- ErgodicAverages.lean 39 declarations
- FiniteMoments.lean 12 declarations
- FourierKernels.lean 24 declarations
- FourierLocalization.lean 38 declarations
- FourierOperators.lean 25 declarations
- FourthMoments.lean 39 declarations
- GaussianAverages.lean 27 declarations
- KernelContinuity.lean 21 declarations
- Main.lean 2 declarations
- Mean.lean 28 declarations
- Model.lean 13 declarations
- ModularCovariance.lean 13 declarations
- PolarCutoff.lean 26 declarations
- PositiveKernels.lean 55 declarations
- RealGraph.lean 45 declarations
- Recovery.lean 13 declarations
- SpectralCalculus.lean 33 declarations
- StrongIntegrals.lean 22 declarations
- StrongLimits.lean 6 declarations
- TomitaFundamental.lean 21 declarations
- TomitaResolvent.lean 46 declarations