OAI/Combinatorics/Progressions/Estimates/PhysicalZeroExtension.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.physical_truncation_restore_difference line 11
  2. theorem OAI.Erdos3.physicalBoxTruncation_congr_on_box line 54
  3. theorem OAI.Erdos3.physicalBoxResidual_congr_on_box line 67
  4. theorem OAI.Erdos3.physicalBoxTruncation_zeroExtend line 80
  5. theorem OAI.Erdos3.physicalBoxResidual_zeroExtend line 89
  6. theorem OAI.Erdos3.physical_zero_extension_restore_difference line 98