OAI/Combinatorics/Progressions/Estimates/RelativeFiberSlicePatch.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.finiteProductIntegral line 13
  2. theorem OAI.Erdos3.finiteProductIntegral_nonneg line 16
  3. theorem OAI.Erdos3.finiteTuple_sum_snoc line 20
  4. theorem OAI.Erdos3.finiteProductIntegral_zero line 29
  5. theorem OAI.Erdos3.finiteProductIntegral_snoc line 36
  6. def OAI.Erdos3.finiteSplitPoint line 60
  7. theorem OAI.Erdos3.finiteSplitPoint_fixed line 64
  8. theorem OAI.Erdos3.finiteSplitPoint_free line 69
  9. theorem OAI.Erdos3.finiteSplitPoint_restrict line 74
  10. theorem OAI.Erdos3.finiteProductIntegral_mono line 89
  11. def OAI.Erdos3.finiteProductCoordinateEquiv line 107
  12. theorem OAI.Erdos3.finiteProductIntegral_reindex line 113
  13. theorem OAI.Erdos3.finiteProductIntegral_split line 139
  14. theorem OAI.Erdos3.finiteProductIntegral_pullback_equiv line 172
  15. def OAI.Erdos3.ResidueBoxSlice.fiberInverseParameters line 195
  16. theorem OAI.Erdos3.ResidueBoxSlice.fiberInverseParameters_degree line 199
  17. def OAI.Erdos3.ResidueBoxSlice.fiberReinsertPatch line 204
  18. theorem OAI.Erdos3.ResidueBoxSlice.fiberReinsertPatch_kernel line 208
  19. theorem OAI.Erdos3.ResidueBoxSlice.fiberReinsertPatch_weight line 211
  20. theorem OAI.Erdos3.ResidueBoxSlice.fiberReinsertPatch_lip line 214
  21. theorem OAI.Erdos3.ResidueBoxSlice.fiberReinsertPatch_value line 217
  22. def OAI.Erdos3.ResidueBoxSlice.fiberIntegerPoint line 227
  23. theorem OAI.Erdos3.ResidueBoxSlice.fiberReinsertPatch_point_value line 231
  24. theorem OAI.Erdos3.ResidueBoxSlice.fiberReinsertPatch_integerPoint_value line 246