OAI/NumberTheory/Ostmann/Conclusion/SelectedPermutation.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Ostmann.Conclusion.two_mul_half_bulkSizeline 14 - def
OAI.Ostmann.Conclusion.selectedLeafPermutationline 19 - theorem
OAI.Ostmann.Conclusion.selectedLeafPermutation_sourceline 24 - def
OAI.Ostmann.Conclusion.selectedCovarianceline 33 - theorem
OAI.Ostmann.Conclusion.selectedAmplitude_sq_le_of_covarianceline 41