OAI/Probability/SKFluctuations/CompContDiff.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

Comp Cont Diff.

  1. theorem OAI.SKFluctuations.Hierarchy.BddSmooth.comp_contDiff line 22
  2. def OAI.SKFluctuations.Hierarchy.smoothAbsPower line 39
  3. theorem OAI.SKFluctuations.Hierarchy.contDiff_smoothAbsPower line 41
  4. theorem OAI.SKFluctuations.Hierarchy.BddSmooth.smoothAbsPower line 46
  5. theorem OAI.SKFluctuations.Hierarchy.potentialLaw_equiv line 58
  6. theorem OAI.SKFluctuations.Hierarchy.potentialLaw_joint_test_eq line 81
  7. theorem OAI.SKFluctuations.Hierarchy.BddSmooth.lineDeriv_comp_contDiff line 98
  8. theorem OAI.SKFluctuations.Hierarchy.variance_comp_le_BddSmooth_block line 108
  9. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchyMean_const_mul line 134
  10. abbrev OAI.SKFluctuations.FeatureIndex line 158
  11. def OAI.SKFluctuations.featureCoefficient line 160
  12. def OAI.SKFluctuations.finiteFeature line 164
  13. theorem OAI.SKFluctuations.finiteFeature_apply line 167
  14. def OAI.SKFluctuations.uniformWeight line 171
  15. theorem OAI.SKFluctuations.uniformWeight_pos line 173
  16. def OAI.SKFluctuations.featureSigns line 176
  17. theorem OAI.SKFluctuations.featureSigns_sq line 181
  18. def OAI.SKFluctuations.featureGauge line 192
  19. theorem OAI.SKFluctuations.featureCoefficient_gauge line 195
  20. theorem OAI.SKFluctuations.finiteFeature_gauge line 204
  21. theorem OAI.SKFluctuations.featureGauge_gaussian line 215
  22. theorem OAI.SKFluctuations.featureGauge_volume line 220
  23. def OAI.SKFluctuations.finiteSKHierarchy line 224
  24. theorem OAI.SKFluctuations.finiteSKHierarchy_gauge line 227
  25. def OAI.SKFluctuations.spinSource line 234
  26. theorem OAI.SKFluctuations.finiteFeature_source line 237
  27. theorem OAI.SKFluctuations.spinSource_gauge line 242
  28. def OAI.SKFluctuations.matrixEmbedding line 254
  29. theorem OAI.SKFluctuations.finiteFeature_matrixEmbedding line 258
  30. theorem OAI.SKFluctuations.spinMean_gauge line 273
  31. theorem OAI.SKFluctuations.spinObservable_gauge line 290
  32. theorem OAI.SKFluctuations.spinDriverSource_gauge line 311
  33. theorem OAI.SKFluctuations.spinEnergy_gauge line 326
  34. abbrev OAI.SKFluctuations.IncrementIndex line 345
  35. abbrev OAI.SKFluctuations.DriverDimension line 346
  36. def OAI.SKFluctuations.prefixDriver line 350
  37. theorem OAI.SKFluctuations.prefixDriver_apply line 355
  38. def OAI.SKFluctuations.driverSigns line 361
  39. theorem OAI.SKFluctuations.driverSigns_sq line 364
  40. def OAI.SKFluctuations.driverGauge line 367
  41. theorem OAI.SKFluctuations.prefixDriver_gauge line 371
  42. def OAI.SKFluctuations.skPinFrame line 384
  43. abbrev OAI.SKFluctuations.skPinFamily line 407
  44. theorem OAI.SKFluctuations.skPinFrame_potential_gauge line 410
  45. theorem OAI.SKFluctuations.skPinFrame_observable_gauge line 418
  46. theorem OAI.SKFluctuations.skPinFrame_energy_gauge line 430
  47. theorem OAI.SKFluctuations.driverQuadratic_gauge line 442
  48. theorem OAI.SKFluctuations.skPinned_joint_test_gauge line 453
  49. theorem OAI.SKFluctuations.Hierarchy.deriv_smoothAbsPower line 479
  50. theorem OAI.SKFluctuations.Hierarchy.deriv_smoothAbsPower_sq_le line 489
  51. theorem OAI.SKFluctuations.Hierarchy.smoothAbsPower_sq line 504
  52. theorem OAI.SKFluctuations.Hierarchy.smoothAbsPower_zero line 511
  53. def OAI.SKFluctuations.Hierarchy.powerEps line 523
  54. theorem OAI.SKFluctuations.Hierarchy.powerEps_pos line 525
  55. theorem OAI.SKFluctuations.Hierarchy.powerEps_le_one line 526
  56. theorem OAI.SKFluctuations.Hierarchy.powerEps_tendsto line 530
  57. theorem OAI.SKFluctuations.Hierarchy.integral_regularized_power_tendsto line 533
  58. theorem OAI.SKFluctuations.Hierarchy.BddSmooth.memLp line 571
  59. theorem OAI.SKFluctuations.Hierarchy.BddSmooth.integrable line 577
  60. theorem OAI.SKFluctuations.Hierarchy.regularized_power_moment_le line 582
  61. theorem OAI.SKFluctuations.Hierarchy.power_moment_le line 626