OAI/Probability/SKFluctuations/PhysicalSusceptibility.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Physical Susceptibility.

  1. theorem OAI.SKFluctuations.Hierarchy.hierarchyMeanPath_terminal line 18
  2. def OAI.SKFluctuations.Hierarchy.lastLayerCut line 29
  3. def OAI.SKFluctuations.Hierarchy.cutIncrements line 34
  4. theorem OAI.SKFluctuations.Hierarchy.sum_cutIncrements line 38
  5. theorem OAI.SKFluctuations.Hierarchy.length_cutIncrements line 48
  6. theorem OAI.SKFluctuations.Hierarchy.lastLayerCut_shift line 54
  7. theorem OAI.SKFluctuations.Hierarchy.lastLayerCut_schedule line 61
  8. theorem OAI.SKFluctuations.Hierarchy.length_layerCutSchedule line 73
  9. theorem OAI.SKFluctuations.spinProjection_actualSpinPath line 86
  10. def OAI.SKFluctuations.physicalSusceptibility line 107
  11. theorem OAI.SKFluctuations.physicalLayerEnergy_projection line 115
  12. theorem OAI.SKFluctuations.actualSpinPath_zero line 126
  13. theorem OAI.SKFluctuations.actualSpinPath_terminal line 132
  14. def OAI.SKFluctuations.fieldProjectionLinearMap line 141
  15. def OAI.SKFluctuations.physicalLayerVectors line 150
  16. theorem OAI.SKFluctuations.sum_physicalLayerVectors line 156
  17. theorem OAI.SKFluctuations.length_physicalLayerVectors line 165
  18. theorem OAI.SKFluctuations.physicalSusceptibility_le_fork_layers line 173
  19. theorem OAI.SKFluctuations.Hierarchy.pathTailTest_terminal_residual line 212
  20. theorem OAI.SKFluctuations.Hierarchy.integral_physical_terminal_residual line 226
  21. def OAI.SKFluctuations.physicalTerminalIncrement line 264
  22. theorem OAI.SKFluctuations.physicalTerminalIncrement_eq_spinPath line 270
  23. theorem OAI.SKFluctuations.physicalTerminalIncrement_measurable line 282
  24. theorem OAI.SKFluctuations.dot_physicalTerminalIncrement line 292
  25. theorem OAI.SKFluctuations.physical_terminal_projection_integrable line 305
  26. theorem OAI.SKFluctuations.eventually_physical_terminal_projection line 342
  27. theorem OAI.SKFluctuations.eventually_physical_suffix_terminal_projection line 382
  28. theorem OAI.SKFluctuations.norm_physicalTerminalIncrement line 446
  29. theorem OAI.SKFluctuations.physicalTerminalIncrement_moment_integrable line 456
  30. theorem OAI.SKFluctuations.Hierarchy.bounded_kernel_power_le line 488
  31. theorem OAI.SKFluctuations.eventually_physical_suffix_random_projection line 541