OAI/Probability/SKFluctuations/PhysicalLayerSum.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

Physical Layer Sum.

  1. def OAI.SKFluctuations.physicalLayerIncrement line 15
  2. theorem OAI.SKFluctuations.sum_physicalLayerIncrement line 22
  3. theorem OAI.SKFluctuations.dot_physicalLayerIncrement line 31
  4. theorem OAI.SKFluctuations.physicalLayerIncrement_dot_sq_integrable line 44
  5. theorem OAI.SKFluctuations.physicalSusceptibility_le_double_sum line 66
  6. def OAI.SKFluctuations.physicalFutureLayerIncrement line 114
  7. def OAI.SKFluctuations.physicalFutureSusceptibility line 120
  8. theorem OAI.SKFluctuations.physicalFutureSusceptibility_le_double_sum line 126
  9. theorem OAI.SKFluctuations.actualSpinPath_source line 165
  10. theorem OAI.SKFluctuations.physicalFutureLayerIncrement_eq_cut line 172
  11. theorem OAI.SKFluctuations.physicalFutureSusceptibility_le_cut_sum line 186
  12. inductive OAI.SKFluctuations.Hierarchy.CutPartition line 213
  13. def OAI.SKFluctuations.Hierarchy.layersOfCuts line 218
  14. theorem OAI.SKFluctuations.Hierarchy.CutPartition.start_le line 222
  15. theorem OAI.SKFluctuations.Hierarchy.CutPartition.all_steps line 228
  16. theorem OAI.SKFluctuations.Hierarchy.length_layersOfCuts line 237
  17. theorem OAI.SKFluctuations.Hierarchy.CutPartition.shifted_schedule line 243
  18. theorem OAI.SKFluctuations.Hierarchy.CutPartition.take_append_layers line 262
  19. theorem OAI.SKFluctuations.Hierarchy.CutPartition.ofFn line 267
  20. theorem OAI.SKFluctuations.cutSlice_mass_le line 291
  21. theorem OAI.SKFluctuations.layersOfCuts_mass_bound line 309
  22. def OAI.SKFluctuations.dyadicRadiusNode line 333
  23. theorem OAI.SKFluctuations.dyadicRadiusNode_zero line 336
  24. theorem OAI.SKFluctuations.dyadicRadiusNode_one line 338
  25. theorem OAI.SKFluctuations.dyadicRadiusNode_succ_succ line 341
  26. theorem OAI.SKFluctuations.dyadicRadiusNode_monotone line 344
  27. theorem OAI.SKFluctuations.dyadicRadiusNode_pos line 355
  28. def OAI.SKFluctuations.dyadicCutIndex line 360
  29. theorem OAI.SKFluctuations.dyadicCutIndex_zero line 363
  30. theorem OAI.SKFluctuations.dyadicCutIndex_one line 365
  31. theorem OAI.SKFluctuations.dyadicCutIndex_end line 367
  32. theorem OAI.SKFluctuations.dyadicCutIndex_terminal line 369
  33. theorem OAI.SKFluctuations.dyadicCutIndex_monotone line 372
  34. theorem OAI.SKFluctuations.dyadicCutIndex_measurable line 383
  35. theorem OAI.SKFluctuations.physicalCutMass_terminal line 391
  36. def OAI.SKFluctuations.physicalDyadicCuts line 397
  37. def OAI.SKFluctuations.physicalDyadicMass line 400
  38. theorem OAI.SKFluctuations.physicalDyadicCuts_partition line 404
  39. theorem OAI.SKFluctuations.physicalDyadicCuts_mass_bound line 417
  40. def OAI.SKFluctuations.physicalQuantileGrid line 445
  41. theorem OAI.SKFluctuations.physicalQuantileGrid_spec line 451
  42. theorem OAI.SKFluctuations.physicalQuantileGrid_mem line 456
  43. theorem OAI.SKFluctuations.physicalQuantileGrid_mono line 461
  44. theorem OAI.SKFluctuations.physicalQuantileGrid_coord line 467
  45. theorem OAI.SKFluctuations.physicalQuantileGrid_last line 472
  46. theorem OAI.SKFluctuations.physicalQuantileGrid_first line 481
  47. theorem OAI.SKFluctuations.physicalQuantileGrid_mesh line 490
  48. theorem OAI.SKFluctuations.sampled_physicalMass_mesh line 517
  49. def OAI.SKFluctuations.radiusGridCut line 542
  50. theorem OAI.SKFluctuations.radiusGridCut_le line 545
  51. theorem OAI.SKFluctuations.radiusGridCut_monotone line 548
  52. theorem OAI.SKFluctuations.radiusGridCut_cell line 557
  53. theorem OAI.SKFluctuations.radiusGridCell_disjoint line 577
  54. theorem OAI.SKFluctuations.exists_radiusGridCell line 595
  55. def OAI.SKFluctuations.radiusGridPoint line 619
  56. theorem OAI.SKFluctuations.radiusGridPoint_bounds line 622
  57. theorem OAI.SKFluctuations.radiusGridPoint_mem line 634
  58. theorem OAI.SKFluctuations.radiusGridPoint_monotone line 638
  59. theorem OAI.SKFluctuations.radiusSampledClock_growth line 643
  60. theorem OAI.SKFluctuations.radiusSampledClock_growth_local line 657