OAI/Analysis/Unitarizability/
356 declarations, 0 contain sorry, 0 declared as axioms; 39 files
Files
- AllDiscrete.lean 1 declarations
- Amenable.lean 2 declarations
- Average.lean 5 declarations
- AveragedForm.lean 12 declarations
- Cocycle.lean 11 declarations
- CompactMean.lean 1 declarations
- ComplexFrames.lean 8 declarations
- Contracting.lean 6 declarations
- DiscreteModel.lean 1 declarations
- EndpointAssignment.lean 10 declarations
- FiniteSigns.lean 9 declarations
- FiniteSynthesis.lean 6 declarations
- FrameParameters.lean 5 declarations
- FrameSelection.lean 2 declarations
- Frames.lean 7 declarations
- HilbertSum.lean 22 declarations
- InvariantProjection.lean 5 declarations
- KernelEnergy.lean 12 declarations
- KernelObstruction.lean 54 declarations
- LocalBounds.lean 12 declarations
- Main.lean 3 declarations
- MaskAlgebra.lean 12 declarations
- Masked.lean 17 declarations
- MeanBounds.lean 5 declarations
- Model.lean 7 declarations
- NearOne.lean 2 declarations
- NetOperator.lean 1 declarations
- Parameters.lean 9 declarations
- Regular.lean 17 declarations
- ScaledObstruction.lean 3 declarations
- SignMatrix.lean 15 declarations
- SparseMask.lean 13 declarations
- SparseSplitting.lean 12 declarations
- SphereNet.lean 2 declarations
- SumObstruction.lean 7 declarations
- Triangular.lean 18 declarations
- Unitarizer.lean 1 declarations
- UniverseTransport.lean 6 declarations
- VectorMean.lean 15 declarations