OAI/Probability/BinarySweep/MatrixBounds/FourierTrace.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BinaryCoordinateSweeps.Fourier.young_trace_resolution line 13
2. theorem OAI.BinaryCoordinateSweeps.Fourier.variation_fourier_bound line 44