`OAI/Probability/ThorpShuffle/`

810 declarations, 0 contain sorry, 0 declared as axioms; 61 files

Folders

FixedLists/ 6 files, 34 declarations

Files

BlockEmbedding.lean 18 declarations
BlockFibers.lean 21 declarations
BlockLaws.lean 2 declarations
Classification.lean 31 declarations
ConditionalFlow.lean 25 declarations
ConditionalLaw.lean 5 declarations
ConvolutionBounds.lean 6 declarations
CosetBounds.lean 7 declarations
Cyclic.lean 17 declarations
DegreeBounds.lean 25 declarations
EightBlocks.lean 7 declarations
EnergyDecay.lean 22 declarations
ExceptionalShapes.lean 4 declarations
ExtensionBounds.lean 10 declarations
FiniteExpectation.lean 19 declarations
FiniteLaw.lean 10 declarations
FirstFourier.lean 3 declarations
FirstMain.lean 1 declarations
FirstMoment.lean 26 declarations
FourierBounds.lean 12 declarations
FourierFamilies.lean 20 declarations
FourierPerturbation.lean 6 declarations
FreshCoins.lean 15 declarations
HalfHistories.lean 24 declarations
Irreducibility.lean 18 declarations
JointProjectors.lean 17 declarations
LinearExtensions.lean 17 declarations
Main.lean 5 declarations
MarginalBounds.lean 7 declarations
MarginalEnergy.lean 18 declarations
MaskedResampling.lean 9 declarations
MixingBounds.lean 7 declarations
Model.lean 19 declarations
NoiseEnergy.lean 24 declarations
PairAveraging.lean 29 declarations
Parity.lean 7 declarations
PartitionBounds.lean 15 declarations
PermutationCharacters.lean 18 declarations
Polytabloids.lean 9 declarations
PrefixTests.lean 3 declarations
ProductProjectors.lean 17 declarations
Reachability.lean 21 declarations
ReciprocalDegrees.lean 19 declarations
Reynolds.lean 19 declarations
Specht.lean 30 declarations
SpectralDecay.lean 7 declarations
Support.lean 12 declarations
SymmetricFamilies.lean 5 declarations
Tableaux.lean 8 declarations
TaggedCompletion.lean 9 declarations
TaggedDeviation.lean 6 declarations
Trimming.lean 21 declarations
VectorOrbits.lean 14 declarations
Walsh.lean 11 declarations
WalshFlow.lean 19 declarations