OAI/Combinatorics/Progressions/Sampling/CanonicalSamplerTuple.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.sigmaAxisSampler line 16
  2. theorem OAI.Erdos3.sigmaAxisSampler_contDiff line 20
  3. theorem OAI.Erdos3.sigmaAxisSampler_hasFDerivAt line 25
  4. theorem OAI.Erdos3.sigmaAxisSampler_fderiv line 35
  5. theorem OAI.Erdos3.sigmaAxisSampler_selectedDerivative line 42
  6. theorem OAI.Erdos3.sigmaAxisSampler_inverse_bound line 50
  7. theorem OAI.Erdos3.sigmaAxisSampler_perturbed_inverse_bound line 61
  8. abbrev OAI.Erdos3.JointBlockParameter line 89
  9. def OAI.Erdos3.jointBooleanSampler line 96
  10. def OAI.Erdos3.jointBooleanInjection line 101
  11. theorem OAI.Erdos3.jointBooleanSampler_contDiff line 107
  12. theorem OAI.Erdos3.jointBooleanInjection_norm_le line 112
  13. theorem OAI.Erdos3.jointBoolean_selectedDerivative_eq line 119
  14. theorem OAI.Erdos3.monomialArrayPolynomial_coeff_abs_le line 143
  15. theorem OAI.Erdos3.jointBooleanSampler_coordinate_abs_le line 150
  16. abbrev OAI.Erdos3.PrincipalTupleIndex line 173
  17. abbrev OAI.Erdos3.SamplerTupleIndex line 176
  18. def OAI.Erdos3.canonicalTupleInput line 179
  19. theorem OAI.Erdos3.canonicalTupleInput_principal line 184
  20. theorem OAI.Erdos3.samplerTupleIndex_card line 188
  21. def OAI.Erdos3.normalizedCubeTuple line 194
  22. theorem OAI.Erdos3.normalizedCubeTuple_principal line 198