OAI/Combinatorics/Progressions/Estimates/ScaledJointFrozenSource.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.jointCubeScale line 13
  2. theorem OAI.Erdos3.jointCubeScale_measurable line 18
  3. def OAI.Erdos3.jointCubeScaleHomeomorph line 22
  4. theorem OAI.Erdos3.jointCubeScaleHomeomorph_apply line 28
  5. def OAI.Erdos3.scaledJointCubeSource line 33
  6. theorem OAI.Erdos3.scaledJointCubeSource_eq_map line 38
  7. theorem OAI.Erdos3.scaledJointCubeSource_probability line 52
  8. theorem OAI.Erdos3.scaledJointCubeSource_integral line 59
  9. def OAI.Erdos3.rawCanonicalCubeTuple line 78
  10. theorem OAI.Erdos3.rawCanonicalCubeTuple_rescale line 85
  11. def OAI.Erdos3.rawCanonicalJet line 97
  12. theorem OAI.Erdos3.rawCanonicalJet_rescale line 109
  13. theorem OAI.Erdos3.scaledJointCubeSource_prod line 137
  14. theorem OAI.Erdos3.scaledJointCubeSource_prod_integral line 147