OAI/Combinatorics/Progressions/Sampling/JointMeasureProductiveNarrowSampler.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.BooleanCubeKernel.physicalSiteWidth_mono line 13
  2. theorem OAI.Erdos3.BooleanCubeKernel.narrowTrimmedSpatialWidths_fit line 19
  3. theorem OAI.Erdos3.BooleanCubeKernel.narrow_jointIntegerPhysicalSite_mem_box line 28
  4. theorem OAI.Erdos3.exists_narrow_sampler_threshold line 50
  5. theorem OAI.Erdos3.narrow_sampler_width_bounds line 72
  6. theorem OAI.Erdos3.narrow_sampler_residue_scale line 95
  7. theorem OAI.Erdos3.BooleanCubeKernel.exists_joint_sampler_uniform_box_law line 137
  8. theorem OAI.Erdos3.BooleanCubeKernel.exists_narrow_joint_sampler line 264
  9. theorem OAI.Erdos3.BooleanCubeKernel.exists_joint_productive_narrow_sampler line 442
  10. theorem OAI.Erdos3.BooleanCubeKernel.exists_productive_narrow_sampler line 565
  11. theorem OAI.Erdos3.BooleanCubeKernel.exists_joint_measure_productive_narrow_sampler line 683