OAI/Probability/SKFluctuations/MarkedAttachPreserves.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

Marked Attach Preserves.

  1. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.markedAttach_preserves line 21
  2. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.markedAttach_tested_hit line 31
  3. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.markedAttach_tested_diagonal line 47
  4. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.markedAttach_zero_diagonal line 68
  5. def OAI.SKFluctuations.Hierarchy.coordinateEquiv line 84
  6. theorem OAI.SKFluctuations.Hierarchy.coordinateEquiv_apply line 88
  7. theorem OAI.SKFluctuations.Hierarchy.coordinateEquiv_measPres line 94
  8. theorem OAI.SKFluctuations.Hierarchy.coordinateEquiv_single line 100
  9. theorem OAI.SKFluctuations.Hierarchy.shiftedContinuation_reindex line 106
  10. theorem OAI.SKFluctuations.Hierarchy.shiftedMean_reindex line 117
  11. def OAI.SKFluctuations.Hierarchy.reindexFeature line 132
  12. theorem OAI.SKFluctuations.Hierarchy.spinWeight_reindex line 135
  13. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchy_clock_reindex line 139
  14. theorem OAI.SKFluctuations.Hierarchy.ClockTree.weight_reindex line 152
  15. def OAI.SKFluctuations.Hierarchy.ClockTree.disorderWeight line 179
  16. theorem OAI.SKFluctuations.Hierarchy.ClockTree.rootWeight_eq_disorder line 185
  17. theorem OAI.SKFluctuations.Hierarchy.ClockTree.disorderWeight_reindex line 192
  18. theorem OAI.SKFluctuations.Hierarchy.ClockTree.disorderWeight_probability line 210
  19. theorem OAI.SKFluctuations.Hierarchy.ClockTree.disorderWeight_cumulative_close line 225
  20. def OAI.SKFluctuations.Hierarchy.ClockTree.disorderExpect line 258
  21. theorem OAI.SKFluctuations.Hierarchy.ClockTree.disorderExpect_close line 264
  22. abbrev OAI.SKFluctuations.OrderedFeatureIndex line 281
  23. def OAI.SKFluctuations.orderedFeatureCoefficient line 283
  24. def OAI.SKFluctuations.orderedFeature line 287
  25. theorem OAI.SKFluctuations.orderedFeature_apply line 290
  26. theorem OAI.SKFluctuations.orderedFeature_single line 294
  27. def OAI.SKFluctuations.orderedAmplitude line 299
  28. theorem OAI.SKFluctuations.orderedAmplitude_nonneg line 303
  29. theorem OAI.SKFluctuations.orderedFeature_abs line 307
  30. theorem OAI.SKFluctuations.orderedFeature_square line 315
  31. def OAI.SKFluctuations.orderedClock line 321
  32. theorem OAI.SKFluctuations.orderedAmplitude_sum line 325
  33. def OAI.SKFluctuations.orderedOverlap line 338
  34. theorem OAI.SKFluctuations.orderedCovariance line 341
  35. theorem OAI.SKFluctuations.Hierarchy.ExpClose.abs_sub_le line 374
  36. theorem OAI.SKFluctuations.Hierarchy.ClockTree.disorderExpect_abs_le line 392
  37. def OAI.SKFluctuations.treeComparisonConstant line 423
  38. theorem OAI.SKFluctuations.treeComparisonConstant_nonneg line 425
  39. def OAI.SKFluctuations.orderedSKWeight line 431
  40. def OAI.SKFluctuations.orderedSKExpect line 435
  41. theorem OAI.SKFluctuations.orderedSKWeight_cumulative_close line 441
  42. theorem OAI.SKFluctuations.orderedSKExpect_cumulative_close line 469
  43. theorem OAI.SKFluctuations.orderedSKExpect_cumulative_abs_le line 487
  44. def OAI.SKFluctuations.Hierarchy.disorderPressure line 515
  45. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchy_boundary_reindex line 521
  46. theorem OAI.SKFluctuations.Hierarchy.disorderPressure_reindex line 533
  47. theorem OAI.SKFluctuations.Hierarchy.disorderPressure_eq_corrected line 552
  48. theorem OAI.SKFluctuations.Hierarchy.disorderPressure_comparison line 559
  49. def OAI.SKFluctuations.orderedSKPressure line 596
  50. theorem OAI.SKFluctuations.orderedSKPressure_comparison line 603