OAI/Combinatorics/Progressions/Estimates/CanonicalEmptyLayerGeometry.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.BooleanCubeKernel.selectedJointReference_collision line 14
  2. theorem OAI.Erdos3.BooleanCubeKernel.selectedJointFiniteLaw_noninjectivity_le line 30
  3. theorem OAI.Erdos3.BooleanCubeKernel.selectedJointFiniteLaw_collision_small line 60
  4. theorem OAI.Erdos3.BooleanCubeKernel.selectedJointReference_trimmed_complex_compare line 97
  5. theorem OAI.Erdos3.BooleanCubeKernel.selectedJointReference_trimmed_compare line 119
  6. theorem OAI.Erdos3.BooleanCubeKernel.selectedJointReference_noninjectivity_le line 137
  7. theorem OAI.Erdos3.zero_slot_score_mean_lower_bound line 169
  8. theorem OAI.Erdos3.productive_finite_samples line 186
  9. theorem OAI.Erdos3.BooleanCubeKernel.exists_unconditioned_productive_family line 237
  10. def OAI.Erdos3.unconditionedResidueSiteBound line 295
  11. def OAI.Erdos3.unconditionedCollisionWidth line 298
  12. theorem OAI.Erdos3.residueBoxIntegerPoint_sum_abs_le line 302
  13. theorem OAI.Erdos3.unconditionedCollisionWidth_pos line 311
  14. theorem OAI.Erdos3.unconditionedCollisionWidth_collision line 319
  15. theorem OAI.Erdos3.BooleanCubeKernel.exists_concrete_unconditioned_productive_family line 330
  16. theorem OAI.Erdos3.relativeBoxInput_expect line 389
  17. theorem OAI.Erdos3.relativePatch_zeroStage_mean_lower_bound line 396
  18. theorem OAI.Erdos3.unconditioned_base_impossibility line 424
  19. def OAI.Erdos3.VectorPolynomial.zeroLayerVariablesEquiv line 475
  20. theorem OAI.Erdos3.VectorPolynomial.zeroLayerVariablesEquiv_inl line 487
  21. theorem OAI.Erdos3.VectorPolynomial.zeroLayerVariablesEquiv_symm line 490
  22. def OAI.Erdos3.VectorPolynomial.zeroLayerSamplerScale line 499
  23. theorem OAI.Erdos3.VectorPolynomial.zeroLayerVariables_card line 506
  24. theorem OAI.Erdos3.VectorPolynomial.allocatedExternalCandidateSides_zero_layers line 512
  25. theorem OAI.Erdos3.VectorPolynomial.allocatedExternalCandidateSides_zero_layers_fun line 519
  26. theorem OAI.Erdos3.VectorPolynomial.allocatedExternalCandidateRootBudget_zero_layers line 524
  27. theorem OAI.Erdos3.VectorPolynomial.allocatedExternalCandidateWidths_zero_layers line 530
  28. def OAI.Erdos3.VectorPolynomial.emptyLayerVariablesEquiv line 558
  29. theorem OAI.Erdos3.VectorPolynomial.emptyLayerVariablesEquiv_inl line 570
  30. theorem OAI.Erdos3.VectorPolynomial.emptyLayerVariablesEquiv_symm line 573
  31. theorem OAI.Erdos3.VectorPolynomial.emptyLayerVariables_card line 582
  32. theorem OAI.Erdos3.VectorPolynomial.allocatedExternalCandidateSides_empty_layers line 588
  33. theorem OAI.Erdos3.VectorPolynomial.allocatedExternalCandidateSides_empty_layers_fun line 595
  34. theorem OAI.Erdos3.VectorPolynomial.allocatedExternalCandidateRootBudget_empty_layers line 600
  35. theorem OAI.Erdos3.VectorPolynomial.allocatedExternalCandidateWidths_empty_layers line 606
  36. theorem OAI.Erdos3.VectorPolynomial.allocatedExternalCandidateWidths_empty_layers_narrowing line 619
  37. theorem OAI.Erdos3.VectorPolynomial.allocatedExternalCandidateSides_sum_zero_layers line 644
  38. theorem OAI.Erdos3.VectorPolynomial.allocatedExternalCandidateWidths_eq_scalar_zero_layers line 650
  39. def OAI.Erdos3.VectorPolynomial.scalarNativeDimension line 666
  40. theorem OAI.Erdos3.VectorPolynomial.scalarNativeDimension_pos line 668
  41. theorem OAI.Erdos3.VectorPolynomial.scalarNativeDimension_capacity line 672
  42. theorem OAI.Erdos3.VectorPolynomial.scalarNativeDimension_selection_bound line 676
  43. def OAI.Erdos3.VectorPolynomial.scalarNativeSelection line 681
  44. theorem OAI.Erdos3.VectorPolynomial.scalarNativeSelection_val line 688
  45. abbrev OAI.Erdos3.VectorPolynomial.CanonicalEmptyLayerGeometry.I line 701
  46. abbrev OAI.Erdos3.VectorPolynomial.CanonicalEmptyLayerGeometry.J line 702
  47. abbrev OAI.Erdos3.VectorPolynomial.CanonicalEmptyLayerGeometry.Q line 703
  48. abbrev OAI.Erdos3.VectorPolynomial.CanonicalEmptyLayerGeometry.n line 704
  49. abbrev OAI.Erdos3.VectorPolynomial.CanonicalEmptyLayerGeometry.B line 706
  50. def OAI.Erdos3.VectorPolynomial.CanonicalEmptyLayerGeometry.U line 708
  51. def OAI.Erdos3.VectorPolynomial.CanonicalEmptyLayerGeometry.b line 710
  52. theorem OAI.Erdos3.VectorPolynomial.CanonicalEmptyLayerGeometry.hb line 714
  53. def OAI.Erdos3.VectorPolynomial.CanonicalEmptyLayerGeometry.o line 718
  54. def OAI.Erdos3.VectorPolynomial.CanonicalEmptyLayerGeometry.bW line 723
  55. instance OAI.Erdos3.VectorPolynomial.CanonicalEmptyLayerGeometry.lattice_full line 728
  56. def OAI.Erdos3.VectorPolynomial.CanonicalEmptyLayerGeometry.poly line 734
  57. theorem OAI.Erdos3.VectorPolynomial.CanonicalEmptyLayerGeometry.poly_mem line 737
  58. theorem OAI.Erdos3.VectorPolynomial.CanonicalEmptyLayerGeometry.poly_degree line 743