OAI/Combinatorics/Progressions/Linear/AllocatedAveragedCoarseKernelComparison.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.character_root_power_cancel_le line 11
  2. theorem OAI.Erdos3.finite_character_reciprocal_tail_of_le line 34
  3. theorem OAI.Erdos3.largeCokernel_reciprocal_probability_le_of_card_le line 57
  4. theorem OAI.Erdos3.boxCokernel_probability_le_of_card_le line 74
  5. theorem OAI.Erdos3.scalarCube_largeCokernel_probability_le_of_card_le line 102
  6. theorem OAI.Erdos3.scalarKernel_explicit_probability_le_of_card_le line 133
  7. theorem OAI.Erdos3.affineKernel_explicit_probability_le_of_card_le line 179
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedTupleEnvelope_ge_input line 215
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalIdealLengthEnvelope_ge_input line 230
  10. theorem OAI.Erdos3.VectorPolynomial.scalarKernelCutoff_le_allocatedPrimitive line 251
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealScale_ge_exp line 275
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedIdealScale_kernel_cutoff line 281
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedReferenceScale_affine_kernel_control line 316
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedNormalizedInitialLog_ge_input line 373
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedPrimitiveNormalizedScale_ge_exp line 390
  16. def OAI.Erdos3.VectorPolynomial.allocatedKernelScale line 397
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedKernelScale_cutoff line 400
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedKernelScale_affine_bad_probability line 423
  19. def OAI.Erdos3.VectorPolynomial.allocatedCoarseKernelScale line 462
  20. theorem OAI.Erdos3.VectorPolynomial.allocatedCoarseKernelScale_cutoff line 465
  21. theorem OAI.Erdos3.VectorPolynomial.allocatedCoarseKernelScale_affine_bad_probability line 479
  22. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginal_kernel_average line 558
  23. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginal_kernel_average_of_bad_bound line 572
  24. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginal_affine_kernel_average line 585
  25. def OAI.Erdos3.VectorPolynomial.allocatedAveragedCoarseKernelStatement line 626
  26. theorem OAI.Erdos3.VectorPolynomial.allocatedAveragedCoarseKernelComparison line 752