OAI/Probability/SKFluctuations/PhysicalPinnedTransport.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Physical Pinned Transport.

  1. theorem OAI.SKFluctuations.physicalPinnedPair_realize line 16
  2. theorem OAI.SKFluctuations.physicalPinnedPair_map_eq line 28
  3. theorem OAI.SKFluctuations.physical_planted_centered_moment_le line 51
  4. theorem OAI.SKFluctuations.physical_planted_variance_le line 76
  5. theorem OAI.SKFluctuations.driverMean_spin line 103
  6. theorem OAI.SKFluctuations.sum_spinSource line 111
  7. theorem OAI.SKFluctuations.driverSource_spin line 119
  8. def OAI.SKFluctuations.physicalSpinL line 127
  9. theorem OAI.SKFluctuations.driverObservable_spin line 132
  10. theorem OAI.SKFluctuations.driverEnergy_spin line 143
  11. theorem OAI.SKFluctuations.physicalNodePair_spin line 151
  12. def OAI.SKFluctuations.physicalCutSusceptibility line 170
  13. theorem OAI.SKFluctuations.physicalCutSusceptibility_at_prefix line 177
  14. theorem OAI.SKFluctuations.physicalCutSusceptibility_nonneg line 188
  15. theorem OAI.SKFluctuations.Hierarchy.cutPredecessor_shift line 207
  16. def OAI.SKFluctuations.Hierarchy.schedulePairSum line 218
  17. theorem OAI.SKFluctuations.Hierarchy.schedulePairSum_shift line 224
  18. theorem OAI.SKFluctuations.physicalPinnedPair_snd_eq_sum line 250
  19. theorem OAI.SKFluctuations.physicalCutSusceptibility_le_schedule line 297
  20. theorem OAI.SKFluctuations.Hierarchy.cutPredecessor_lookup line 332
  21. theorem OAI.SKFluctuations.Hierarchy.cutPredecessor_ofFn line 341
  22. theorem OAI.SKFluctuations.Hierarchy.schedulePairSum_ofFn line 354
  23. theorem OAI.SKFluctuations.physicalCutSusceptibility_le_array line 373
  24. theorem OAI.SKFluctuations.projection_weight_scale_bound line 402
  25. theorem OAI.SKFluctuations.integral_weighted_power_root line 426
  26. theorem OAI.SKFluctuations.eventually_weighted_far_pair_moment line 433
  27. theorem OAI.SKFluctuations.Hierarchy.integral_power_root_le_mass line 476
  28. theorem OAI.SKFluctuations.physicalCutPairSquare_joint line 533
  29. def OAI.SKFluctuations.HasFarPairClock line 546
  30. def OAI.SKFluctuations.physicalCutPairRadiusIntegral line 553
  31. theorem OAI.SKFluctuations.eventually_physical_far_radius_integral line 558
  32. theorem OAI.SKFluctuations.eventually_physical_far_mass_integral line 614