OAI/Combinatorics/Progressions/Lattices/AffineCubeMinorGoodMass.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.affine_preimage_volume_real line 15
  2. theorem OAI.Erdos3.affine_sublevel_volume_real line 23
  3. theorem OAI.Erdos3.exists_affine_boolean_minor_sublevel_bound line 38
  4. def OAI.Erdos3.reindexedAffineSource line 73
  5. theorem OAI.Erdos3.reindexedAffineSource_continuous line 77
  6. theorem OAI.Erdos3.reindexedAffineSource_apply line 83
  7. theorem OAI.Erdos3.exists_affine_cube_minor_probability_bound line 89
  8. theorem OAI.Erdos3.booleanMinorDeterminant_affine_sublevel_marginal line 118
  9. theorem OAI.Erdos3.inverseJacobian_coordinateScale_le line 155
  10. theorem OAI.Erdos3.exists_allocated_affine_cube_minor_probability_bound line 171
  11. def OAI.Erdos3.affineCubeMinorThreshold line 238
  12. theorem OAI.Erdos3.affineCubeMinorThreshold_pos line 244
  13. theorem OAI.Erdos3.affineCubeMinorThreshold_log_inv line 252
  14. theorem OAI.Erdos3.exists_affine_cube_minor_thresholds line 263
  15. lemma OAI.Erdos3.log_one_add_inverse_width_pow line 322
  16. theorem OAI.Erdos3.affineCubeMinorThreshold_log_inv_slice_bound line 333
  17. def OAI.Erdos3.affineBooleanCubeDeterminant line 365
  18. theorem OAI.Erdos3.affineBooleanCubeDeterminant_contDiff line 372
  19. def OAI.Erdos3.affineBooleanCubeGoodWeight line 381
  20. def OAI.Erdos3.affineBooleanCubeCutoff line 391
  21. theorem OAI.Erdos3.affineBooleanCubeCutoff_contDiff line 408
  22. theorem OAI.Erdos3.affineBooleanCubeCutoff_range line 414
  23. theorem OAI.Erdos3.affineBooleanCubeGoodWeight_spec line 419
  24. theorem OAI.Erdos3.affineBooleanCubeGoodWeight_integral_test line 442
  25. theorem OAI.Erdos3.affineBooleanCubeGoodWeight_measure line 452
  26. theorem OAI.Erdos3.affineBooleanCubeGoodWeight_mass_lower line 474
  27. theorem OAI.Erdos3.affineBooleanCubeDeterminant_fderiv_norm_le line 512
  28. theorem OAI.Erdos3.affineBooleanCubeGoodWeight_derivative_budget line 537
  29. theorem OAI.Erdos3.exists_affine_cube_good_mass line 579