OAI/Analysis/TemperedDistribution/ConformalIdentities.lean

GitHub source file

75 declarations, 0 contain sorry, 0 declared as axioms

Four-dimensional tempered-distribution improvement and conformal-current identities.

  1. def OAI.ScaleConformal.exponentialCharacter line 14
  2. theorem OAI.ScaleConformal.exponentialCharacter_injective line 19
  3. theorem OAI.ScaleConformal.exponentialWeights_independent line 26
  4. theorem OAI.ScaleConformal.finite_exponential_coefficients line 31
  5. theorem OAI.ScaleConformal.finite_weight_selection line 44
  6. theorem OAI.ScaleConformal.finsupp_weight_selection line 62
  7. theorem OAI.ScaleConformal.schwartz_derivatives_commute line 87
  8. theorem OAI.ScaleConformal.distribution_derivatives_commute line 100
  9. def OAI.ScaleConformal.functionDerivative line 106
  10. theorem OAI.ScaleConformal.fderiv_temperate line 109
  11. theorem OAI.ScaleConformal.functionDerivative_temperate line 115
  12. theorem OAI.ScaleConformal.schwartz_multiplier_derivative line 119
  13. theorem OAI.ScaleConformal.distribution_multiplier_derivative line 134
  14. abbrev OAI.ScaleConformal.Spacetime line 148
  15. def OAI.ScaleConformal.coordinateVector line 150
  16. def OAI.ScaleConformal.metricSign line 152
  17. def OAI.ScaleConformal.metric line 154
  18. theorem OAI.ScaleConformal.metric_diagonal line 156
  19. theorem OAI.ScaleConformal.metric_sign_sq line 159
  20. theorem OAI.ScaleConformal.metric_symmetric line 163
  21. abbrev OAI.ScaleConformal.Distribution line 171
  22. abbrev OAI.ScaleConformal.Tensor line 174
  23. def OAI.ScaleConformal.pd line 177
  24. theorem OAI.ScaleConformal.partial_add line 179
  25. theorem OAI.ScaleConformal.partial_sub line 182
  26. theorem OAI.ScaleConformal.partial_smul line 186
  27. theorem OAI.ScaleConformal.partial_zero line 189
  28. theorem OAI.ScaleConformal.partial_sum line 192
  29. theorem OAI.ScaleConformal.partial_commute line 196
  30. def OAI.ScaleConformal.wave line 200
  31. def OAI.ScaleConformal.trace line 203
  32. def OAI.ScaleConformal.divergence line 206
  33. def OAI.ScaleConformal.correction line 209
  34. def OAI.ScaleConformal.improved line 212
  35. def OAI.ScaleConformal.SymmetricTensor line 215
  36. def OAI.ScaleConformal.ConservedTensor line 217
  37. theorem OAI.ScaleConformal.correction_symmetric line 219
  38. theorem OAI.ScaleConformal.partial_wave line 223
  39. theorem OAI.ScaleConformal.metric_contract line 230
  40. theorem OAI.ScaleConformal.correction_conserved line 235
  41. theorem OAI.ScaleConformal.correction_trace line 246
  42. theorem OAI.ScaleConformal.improvement_identities line 256
  43. def OAI.ScaleConformal.multiply line 272
  44. theorem OAI.ScaleConformal.multiply_zero line 275
  45. theorem OAI.ScaleConformal.multiply_add line 278
  46. theorem OAI.ScaleConformal.multiply_sub line 281
  47. theorem OAI.ScaleConformal.multiply_smul line 284
  48. theorem OAI.ScaleConformal.multiply_sum line 287
  49. theorem OAI.ScaleConformal.multiply_add_function line 291
  50. theorem OAI.ScaleConformal.multiply_smul_function line 296
  51. abbrev OAI.ScaleConformal.CovectorField line 301
  52. abbrev OAI.ScaleConformal.fpd line 303
  53. def OAI.ScaleConformal.vectorDivergence line 306
  54. def OAI.ScaleConformal.TemperateVectorField line 309
  55. def OAI.ScaleConformal.ConformalKilling line 312
  56. theorem OAI.ScaleConformal.vectorDivergence_temperate line 315
  57. def OAI.ScaleConformal.current line 324
  58. def OAI.ScaleConformal.currentDivergence line 327
  59. def OAI.ScaleConformal.derivativeContraction line 330
  60. theorem OAI.ScaleConformal.current_divergence_product_rule line 333
  61. theorem OAI.ScaleConformal.derivativeContraction_swap line 352
  62. theorem OAI.ScaleConformal.conformal_killing_contraction line 363
  63. theorem OAI.ScaleConformal.conformal_current_divergence line 400
  64. theorem OAI.ScaleConformal.conformal_current_conserved line 408
  65. structure OAI.ScaleConformal.AffineKillingVector line 417
  66. def OAI.ScaleConformal.AffineKillingVector.field line 422
  67. theorem OAI.ScaleConformal.AffineKillingVector.derivative line 425
  68. theorem OAI.ScaleConformal.AffineKillingVector.diagonal line 432
  69. theorem OAI.ScaleConformal.AffineKillingVector.temperate line 437
  70. theorem OAI.ScaleConformal.AffineKillingVector.divergence line 441
  71. theorem OAI.ScaleConformal.AffineKillingVector.conformalKilling line 446
  72. def OAI.ScaleConformal.affineSuperpotential line 453
  73. theorem OAI.ScaleConformal.affineSuperpotential_antisymmetric line 458
  74. theorem OAI.ScaleConformal.correction_current line 465
  75. theorem OAI.ScaleConformal.affine_superpotential_identity line 478