OAI/Combinatorics/Progressions/Linear/AllocatedKernelScaleWithCutoff.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.kernelExponentEmbedding line 14
  2. abbrev OAI.Erdos3.VectorPolynomial.NonkernelCoefficient line 24
  3. def OAI.Erdos3.VectorPolynomial.kernelCoefficientEquiv line 27
  4. theorem OAI.Erdos3.VectorPolynomial.kernelCoefficientEquiv_inl line 31
  5. theorem OAI.Erdos3.VectorPolynomial.kernelCoefficientEquiv_inr line 34
  6. theorem OAI.Erdos3.VectorPolynomial.monomialScale_kernelExponent line 37
  7. theorem OAI.Erdos3.VectorPolynomial.kernelExponent_eval_monomial line 43
  8. theorem OAI.Erdos3.VectorPolynomial.integerMappedCubeTuple_kernel line 51
  9. theorem OAI.Erdos3.VectorPolynomial.integerMappedJetMatrix_kernel line 60
  10. theorem OAI.Erdos3.VectorPolynomial.integerMappedJetMatrix_kernel_split line 76
  11. theorem OAI.Erdos3.VectorPolynomial.normalizedIntegerColumns_eq_of_instances line 99
  12. theorem OAI.Erdos3.VectorPolynomial.kernelExponent_eval_real line 111
  13. theorem OAI.Erdos3.VectorPolynomial.normalizedMappedKernelJet_eq line 119
  14. theorem OAI.Erdos3.normalizedJoinedMatrix_affineJetUnitMap line 155
  15. theorem OAI.Erdos3.normalizedJoinedMatrix_affineDensity_law line 181
  16. abbrev OAI.Erdos3.VectorPolynomial.AllocatedNonkernelCoefficient line 217
  17. def OAI.Erdos3.VectorPolynomial.allocatedKernelCoefficientEquiv line 220
  18. def OAI.Erdos3.VectorPolynomial.allocatedNonkernelExponent line 225
  19. theorem OAI.Erdos3.VectorPolynomial.allocatedNonkernelExponent_degree line 229
  20. theorem OAI.Erdos3.VectorPolynomial.allocatedKernelCoefficientScale line 237
  21. theorem OAI.Erdos3.VectorPolynomial.allocatedKernelCoefficientScales_split line 247
  22. theorem OAI.Erdos3.VectorPolynomial.allocatedKernelProfile_bound line 266
  23. theorem OAI.Erdos3.VectorPolynomial.allocatedKernelProfile_sum_pos line 271
  24. theorem OAI.Erdos3.VectorPolynomial.allocatedKernel_image_law line 276
  25. theorem OAI.Erdos3.VectorPolynomial.allocatedKernelJet_split line 295
  26. theorem OAI.Erdos3.VectorPolynomial.allocatedKernelJet_full_image line 309
  27. theorem OAI.Erdos3.VectorPolynomial.allocatedKernelJet_image_law line 324
  28. def OAI.Erdos3.VectorPolynomial.allocatedContinuousProfileCenters line 368
  29. def OAI.Erdos3.VectorPolynomial.allocatedContinuousProfileWidths line 373
  30. def OAI.Erdos3.VectorPolynomial.allocatedContinuousProfileScales line 385
  31. theorem OAI.Erdos3.VectorPolynomial.allocatedContinuousProfileScales_pos line 389
  32. theorem OAI.Erdos3.VectorPolynomial.allocatedContinuousProfileWidths_pos line 395
  33. theorem OAI.Erdos3.VectorPolynomial.allocatedContinuousProfile_bound line 401
  34. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerCenters_scale line 407
  35. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerWidths_scale line 414
  36. theorem OAI.Erdos3.VectorPolynomial.allocatedContinuousProfileScales_split line 421
  37. theorem OAI.Erdos3.VectorPolynomial.allocatedContinuous_reindexed_image_law line 441
  38. theorem OAI.Erdos3.VectorPolynomial.allocatedPartitionedInput_normalized line 473
  39. def OAI.Erdos3.VectorPolynomial.allocatedContinuousKernelDensity line 490
  40. theorem OAI.Erdos3.VectorPolynomial.allocatedContinuousKernel_image_law line 502
  41. theorem OAI.Erdos3.VectorPolynomial.allocatedInteger_replacementScale_le line 551
  42. def OAI.Erdos3.allocatedUnitProfileWidth line 586
  43. theorem OAI.Erdos3.allocatedUnitProfileWidth_pos line 589
  44. theorem OAI.Erdos3.allocatedUnitProfileWidth_le line 593
  45. theorem OAI.Erdos3.allocatedUnitProfileWidth_inverse_exp line 611
  46. theorem OAI.Erdos3.VectorPolynomial.allocatedContinuousProfileWidths_floor line 637
  47. theorem OAI.Erdos3.VectorPolynomial.allocatedPartitionedInput_frozen_bound line 670
  48. theorem OAI.Erdos3.VectorPolynomial.allocatedContinuousKernelDensity_measurable line 678
  49. theorem OAI.Erdos3.VectorPolynomial.allocatedContinuousKernelDensity_probability_data line 690
  50. theorem OAI.Erdos3.VectorPolynomial.allocatedContinuousKernelDensity_bounds line 701
  51. def OAI.Erdos3.VectorPolynomial.AllocatedTailCutoffCompatible line 737
  52. theorem OAI.Erdos3.VectorPolynomial.allocatedTailCutoffCompatible_of_le line 741
  53. theorem OAI.Erdos3.VectorPolynomial.allocatedTailCutoffCompatible_of_moderate line 747
  54. theorem OAI.Erdos3.VectorPolynomial.allocatedInteger_replacementScale_le_withCutoff line 755