OAI/Combinatorics/Progressions/Linear/PhysicalJetTentKernel.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.ambientTentKernel line 15
  2. theorem OAI.Erdos3.ambientTentKernel_symm line 18
  3. theorem OAI.Erdos3.ambientTentKernel_support line 23
  4. theorem OAI.Erdos3.ambientTentKernel_range line 36
  5. theorem OAI.Erdos3.normalizedAmbientTent_shift_lipschitz line 43
  6. theorem OAI.Erdos3.ambientTentKernel_continuous line 52
  7. theorem OAI.Erdos3.ambientTentKernel_integrable line 57
  8. theorem OAI.Erdos3.ambientTentKernel_integral line 63
  9. def OAI.Erdos3.finiteKernelObservable line 87
  10. theorem OAI.Erdos3.finiteKernelObservable_measurable line 90
  11. theorem OAI.Erdos3.finiteKernelObservable_norm_le line 96
  12. theorem OAI.Erdos3.finiteKernelObservable_integral line 108
  13. theorem OAI.Erdos3.finiteKernelObservable_integrable line 128
  14. theorem OAI.Erdos3.finiteKernelObservable_source_error line 136
  15. theorem OAI.Erdos3.ambientTentKernel_lipschitz_error line 172
  16. theorem OAI.Erdos3.finiteAmbientKernel_transfer line 209
  17. theorem OAI.Erdos3.majorant_reweight_norm line 277
  18. theorem OAI.Erdos3.majorant_reweight_exact line 285
  19. theorem OAI.Erdos3.finiteAmbientMajorant_transfer line 300
  20. def OAI.Erdos3.VectorPolynomial.coveredJetAmbientHom line 341
  21. def OAI.Erdos3.BooleanCubeKernel.physicalJetTentKernel line 364
  22. theorem OAI.Erdos3.BooleanCubeKernel.physicalJetTentKernel_properties line 369
  23. theorem OAI.Erdos3.BooleanCubeKernel.exists_physicalJetTent_fourier line 385