OAI/Probability/ParisiFinite/MovingTensorInsertionLimit.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

Moving Tensor Insertion Limit.

  1. theorem OAI.FiniteTensor.moving_tensor_insertion_limit line 27
  2. def OAI.CoherentFock.exponential line 67
  3. theorem OAI.CoherentFock.inner_exponential line 70
  4. theorem OAI.CoherentFock.W_exponential line 79
  5. theorem OAI.QuantumCLT.weylProduct_exponential line 96
  6. theorem OAI.QuantumCLT.weylProduct_exponential_pairing line 117
  7. theorem OAI.FiniteTensor.moving_tensor_weyl_limit line 135
  8. theorem OAI.CoherentFock.tendsto_inner_of_coherent_tests line 190
  9. theorem OAI.CoherentFock.tendsto_of_coherent_tests_and_norm line 224
  10. theorem OAI.CoherentFock.tendsto_unitary_inverse line 249
  11. theorem OAI.FourierDensity.character_memLp line 269
  12. def OAI.FourierDensity.characterVector line 273
  13. theorem OAI.FourierDensity.characterVector_ae line 275
  14. theorem OAI.FourierDensity.character_span_dense line 281
  15. theorem OAI.FourierDensity.exists_character_approx line 305
  16. def OAI.FourierDensity.realPart line 324
  17. theorem OAI.FourierDensity.realPart_ae line 327
  18. theorem OAI.FourierDensity.realPart_norm line 332
  19. def OAI.FourierDensity.oddPart line 337
  20. theorem OAI.FourierDensity.oddPart_ae line 343
  21. theorem OAI.FourierDensity.oddPart_norm line 361
  22. theorem OAI.FourierDensity.oddPart_eq line 371
  23. def OAI.FourierDensity.sine line 378
  24. theorem OAI.FourierDensity.sine_memLp line 380
  25. def OAI.FourierDensity.sineVector line 386
  26. theorem OAI.FourierDensity.sineVector_ae line 388
  27. theorem OAI.FourierDensity.oddPart_realPart_character line 393
  28. theorem OAI.FourierDensity.exists_odd_sine_approx line 419
  29. def OAI.FourierDensity.sinePolynomial line 448
  30. theorem OAI.FourierDensity.sinePolynomial_odd line 452
  31. theorem OAI.FourierDensity.sinePolynomial_bounded line 457
  32. theorem OAI.FourierDensity.sinePolynomial_contDiff line 469
  33. theorem OAI.FourierDensity.sinePolynomial_ae line 481
  34. def OAI.FourierDensity.sineOutput line 498
  35. theorem OAI.FourierDensity.sineOutput_memLp line 501
  36. def OAI.FourierDensity.sineOutputVector line 508
  37. theorem OAI.FourierDensity.sineOutputVector_ae line 511
  38. theorem OAI.FourierDensity.exists_sine_angle_approx line 517
  39. def OAI.FourierDensity.frequency line 572
  40. theorem OAI.FourierDensity.frequency_apply line 575
  41. theorem OAI.FourierDensity.sine_norm_sub_le line 578
  42. theorem OAI.FourierDensity.sinePolynomial_lipschitz_bound line 587
  43. theorem OAI.FourierDensity.iterated_sine_cosine_bound line 603
  44. theorem OAI.FourierDensity.sine_derivative_bound line 613
  45. theorem OAI.FourierDensity.sinePolynomial_derivative_bound line 629