OAI/Probability/SKBarriers/Gaussian/BlockStein.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SK.Analytic.normalizedDot line 15
  2. def OAI.SK.Analytic.normalizedSquare line 17
  3. theorem OAI.SK.Analytic.normalizedSquare_nonneg line 19
  4. theorem OAI.SK.Analytic.normalizedSquare_le_one line 22
  5. theorem OAI.SK.Analytic.normalizedDot_self line 35
  6. theorem OAI.SK.Analytic.normalizedDot_sq_le line 38
  7. theorem OAI.SK.Analytic.abs_normalizedDot_le line 44
  8. theorem OAI.SK.Analytic.normalizedDot_sub_right line 50
  9. theorem OAI.SK.Analytic.normalizedDot_add_left line 54
  10. theorem OAI.SK.Analytic.normalizedDot_comm line 58
  11. theorem OAI.SK.Analytic.mean_cross_replacement line 61
  12. theorem OAI.SK.Analytic.mean_square_replacement line 72
  13. theorem OAI.SK.Analytic.mean_variance_replacement line 96
  14. def OAI.SK.Analytic.hierarchyMeanSquare line 129
  15. theorem OAI.SK.Analytic.hierarchyMeanSquare_bounds line 133
  16. theorem OAI.SK.Analytic.hierarchyMeanSquare_fixed line 141
  17. theorem OAI.SK.Analytic.hierarchyMeanSquare_eq_gradient line 148
  18. theorem OAI.SK.Analytic.hierarchyMeanSquare_regular line 158
  19. theorem OAI.SK.Analytic.hierarchyMeanSquare_invariant line 178
  20. theorem OAI.SK.Analytic.hierarchyMeanSquare_stein line 193
  21. def OAI.SK.Analytic.hierarchyMeanOverlap line 226
  22. theorem OAI.SK.Analytic.hierarchyMeanSquare_continuous line 230
  23. theorem OAI.SK.Analytic.hierarchyMeanSquare_integrable line 239
  24. theorem OAI.SK.Analytic.hierarchyMeanOverlap_bounds line 250
  25. theorem OAI.SK.Analytic.hierarchyMean_increment_identity line 263
  26. theorem OAI.SK.Analytic.hierarchyMeanOverlap_mono line 303
  27. def OAI.SK.Analytic.massFromAtoms line 316
  28. theorem OAI.SK.Analytic.massFromAtoms_castSucc line 319
  29. theorem OAI.SK.Analytic.massFromAtoms_last line 327
  30. theorem OAI.SK.Analytic.hierarchyAtom_massFromAtoms line 336
  31. theorem OAI.SK.Analytic.massFromAtoms_nonneg line 348
  32. theorem OAI.SK.Analytic.massFromAtoms_le_sum line 356
  33. theorem OAI.SK.Analytic.massFromAtoms_monotone line 364
  34. abbrev OAI.SK.Analytic.blockDimension line 379
  35. def OAI.SK.Analytic.fieldIndex line 381
  36. def OAI.SK.Analytic.blockLevel line 387
  37. theorem OAI.SK.Analytic.fieldIndex_val line 393
  38. theorem OAI.SK.Analytic.blockLevel_val line 395
  39. theorem OAI.SK.Analytic.fieldIndex_injective line 398
  40. theorem OAI.SK.Analytic.blockLevel_injective line 416
  41. theorem OAI.SK.Analytic.fieldIndex_lt_level line 424
  42. theorem OAI.SK.Analytic.fieldIndex_mono_block line 429
  43. theorem OAI.SK.Analytic.blockLevel_mono line 434
  44. def OAI.SK.Analytic.blockAtom line 439
  45. theorem OAI.SK.Analytic.blockAtom_nonneg line 442
  46. theorem OAI.SK.Analytic.blockAtom_sum line 448
  47. theorem OAI.SK.Analytic.blockAtom_at line 455
  48. theorem OAI.SK.Analytic.blockAtom_zero_off line 462
  49. def OAI.SK.Analytic.blockMass line 466
  50. theorem OAI.SK.Analytic.blockMass_valid line 468
  51. theorem OAI.SK.Analytic.hierarchyAtom_blockMass line 475
  52. theorem OAI.SK.Analytic.blockLevel_outside_pair line 480
  53. theorem OAI.SK.Analytic.blockLevel_prefix_second line 494
  54. def OAI.SK.Analytic.pairCoefficients line 502
  55. theorem OAI.SK.Analytic.coordinateVector_pair line 505
  56. theorem OAI.SK.Analytic.coordinateLinear_pair line 510
  57. def OAI.SK.Analytic.sharedFieldCoefficients line 516
  58. def OAI.SK.Analytic.retainedFieldDirection line 520
  59. theorem OAI.SK.Analytic.retainedFieldDirection_spin line 532
  60. theorem OAI.SK.Analytic.sharedField_termination line 537
  61. theorem OAI.SK.Analytic.sharedField_level_invariant line 545
  62. theorem OAI.SK.Analytic.sharedField_atom_cancellation line 555
  63. theorem OAI.SK.Analytic.blockMeanSquare_stein line 571