OAI/Probability/SKFluctuations/CavityFrozenJet.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

Cavity Frozen Jet.

  1. def OAI.SKFluctuations.Cavity.cutFrozenLowHighJet line 23
  2. theorem OAI.SKFluctuations.Cavity.cutFrozenLowHighJet_continuous line 30
  3. theorem OAI.SKFluctuations.Cavity.cutFrozenLowHighJet_endpoint line 37
  4. def OAI.SKFluctuations.Cavity.cutFrozenCenteredJet line 46
  5. theorem OAI.SKFluctuations.Cavity.cutFrozenCenteredJet_continuous line 54
  6. theorem OAI.SKFluctuations.Cavity.cutFrozenCenteredJet_endpoint line 60
  7. theorem OAI.SKFluctuations.Cavity.cutFrozenLowHighJet_hasDerivAt line 70
  8. theorem OAI.SKFluctuations.Cavity.cutFrozenCenteredJet_hasDerivAt line 90
  9. theorem OAI.SKFluctuations.Cavity.cutCenteredJet_frozen_decomposition line 100
  10. def OAI.SKFluctuations.Hierarchy.ClockTree.CutGauge line 142
  11. def OAI.SKFluctuations.Hierarchy.ClockTree.assignmentGauge line 151
  12. def OAI.SKFluctuations.Hierarchy.ClockTree.cutGaugeEquiv line 157
  13. theorem OAI.SKFluctuations.Hierarchy.ClockTree.weight_gauge line 167
  14. theorem OAI.SKFluctuations.Hierarchy.gaussian_coordinate_zero_ae line 201
  15. theorem OAI.SKFluctuations.Hierarchy.ClockTree.weight_cutGauge line 208
  16. theorem OAI.SKFluctuations.Hierarchy.ClockTree.cutGaugeEquiv_zero_cases line 256
  17. theorem OAI.SKFluctuations.Hierarchy.ClockTree.weight_cutGauge_endpoint line 265
  18. theorem OAI.SKFluctuations.Hierarchy.ClockTree.expect_cutGauge_odd line 315
  19. theorem OAI.SKFluctuations.Cavity.rowDriverFlip_gaussian_fixed_ae line 340
  20. theorem OAI.SKFluctuations.Cavity.cutFullVariance_zero_scalar line 350
  21. theorem OAI.SKFluctuations.Cavity.cutFullVariance_zero_row line 355
  22. theorem OAI.SKFluctuations.Cavity.cutDisorderWeight_gauge line 362
  23. theorem OAI.SKFluctuations.Cavity.cutDisorderExpect_odd line 402
  24. def OAI.SKFluctuations.Hierarchy.ClockTree.Slot line 424
  25. def OAI.SKFluctuations.Hierarchy.ClockTree.atSlot line 429
  26. def OAI.SKFluctuations.Hierarchy.ClockTree.splitIndex line 434
  27. theorem OAI.SKFluctuations.Hierarchy.ClockTree.splitIndex_self line 441
  28. def OAI.SKFluctuations.Hierarchy.ClockTree.offGauge line 448
  29. def OAI.SKFluctuations.Hierarchy.ClockTree.gaugeAt line 456
  30. theorem OAI.SKFluctuations.Hierarchy.ClockTree.atSlot_assignmentGauge line 466
  31. theorem OAI.SKFluctuations.Hierarchy.ClockTree.cutGaugeEquiv_off line 474
  32. theorem OAI.SKFluctuations.Hierarchy.ClockTree.atSlot_gaugeAt line 490
  33. def OAI.SKFluctuations.Hierarchy.ClockTree.cavityRightSlot line 524
  34. theorem OAI.SKFluctuations.Hierarchy.ClockTree.atSlot_cavityRight line 529
  35. theorem OAI.SKFluctuations.Hierarchy.ClockTree.cavityAssignment_gauge_left line 537
  36. theorem OAI.SKFluctuations.Hierarchy.ClockTree.cavityAssignment_cutGauge_left line 546
  37. def OAI.SKFluctuations.Cavity.sitePair line 576
  38. theorem OAI.SKFluctuations.Cavity.sitePair_apply line 581
  39. theorem OAI.SKFluctuations.Cavity.cutDisorderExpect_sitePair_zero line 589
  40. theorem OAI.SKFluctuations.Cavity.scalarSitePair_zero line 609