OAI/Combinatorics/Progressions/Lattices/AffineBooleanCubeComparison.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.affineSelectedInjection line 12
  2. theorem OAI.Erdos3.affineSelectedInjection_norm_le line 16
  3. theorem OAI.Erdos3.selectedDerivative_affine line 29
  4. theorem OAI.Erdos3.invertible_smul_inverse line 42
  5. theorem OAI.Erdos3.selectedDerivative_affine_inverse_bound line 53
  6. theorem OAI.Erdos3.selectedDerivative_affine_derivative_bound line 68
  7. def OAI.Erdos3.jointAffineBooleanSampler line 113
  8. def OAI.Erdos3.jointAffineBooleanInjection line 120
  9. theorem OAI.Erdos3.jointAffineBooleanSampler_contDiff line 135
  10. theorem OAI.Erdos3.jointAffineBooleanInjection_norm_le line 142
  11. theorem OAI.Erdos3.jointAffineBoolean_selected_inverse_bound line 149
  12. theorem OAI.Erdos3.jointAffineBoolean_selected_derivative_bound line 173
  13. theorem OAI.Erdos3.jointAffineBoolean_c2_error_transport line 211
  14. theorem OAI.Erdos3.affineBooleanCube_comparison line 258