OAI/Combinatorics/Progressions/Sampling/FullParameterJointSampler.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Erdos3.BooleanCubeKernel.exists_explicit_selected_sampler_marginalsline 16 - theorem
OAI.Erdos3.BooleanCubeKernel.exists_explicit_joint_sampler_marginalsline 159 - theorem
OAI.Erdos3.BooleanCubeKernel.exists_explicit_joint_sampler_with_collisionsline 305 - theorem
OAI.Erdos3.BooleanCubeKernel.exists_full_parameter_joint_samplerline 479