OAI/Probability/SKFluctuations/PositiveMass.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Positive Mass.

  1. abbrev OAI.SKFluctuations.Hierarchy.PositiveMass line 20
  2. def OAI.SKFluctuations.Hierarchy.HeatJet.boundarySchedule line 23
  3. def OAI.SKFluctuations.Hierarchy.boundaryCost line 28
  4. theorem OAI.SKFluctuations.Hierarchy.HeatJet.boundarySchedule_gradient_bound line 33
  5. theorem OAI.SKFluctuations.Hierarchy.HeatJet.boundary_head_move line 44
  6. theorem OAI.SKFluctuations.Hierarchy.HeatJet.boundarySchedule_comparison line 72
  7. theorem OAI.SKFluctuations.Hierarchy.boundaryCost_le line 127
  8. theorem OAI.SKFluctuations.Hierarchy.boundaryCost_uniform line 148
  9. theorem OAI.SKFluctuations.Hierarchy.HeatJet.cumulativeClock_uniform line 160
  10. def OAI.SKFluctuations.Hierarchy.diagonalBoundarySteps line 179
  11. theorem OAI.SKFluctuations.Hierarchy.diagonalBoundarySteps_ordered line 184
  12. def OAI.SKFluctuations.Hierarchy.diagonalBoundaryPotential line 197
  13. theorem OAI.SKFluctuations.Hierarchy.diagonalBoundary_head_move line 202
  14. theorem OAI.SKFluctuations.Hierarchy.diagonalBoundary_comparison line 245
  15. theorem OAI.SKFluctuations.Hierarchy.diagonalBoundary_uniform line 323
  16. theorem OAI.SKFluctuations.Hierarchy.shiftedContinuation_tendsto_zero_mass line 349
  17. def OAI.SKFluctuations.Hierarchy.diagonalRootBoundary line 371
  18. theorem OAI.SKFluctuations.Hierarchy.diagonalRoot_uniform line 378
  19. theorem OAI.SKFluctuations.Hierarchy.finiteLinear_eq_sum line 433
  20. theorem OAI.SKFluctuations.Hierarchy.integral_exp_finiteLinear line 442
  21. theorem OAI.SKFluctuations.Hierarchy.spinLogPartition_mass_one line 465
  22. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchy_append_mass_one line 498
  23. def OAI.SKFluctuations.Hierarchy.diagonalPointSteps line 521
  24. theorem OAI.SKFluctuations.Hierarchy.diagonalPointSteps_cons line 524
  25. theorem OAI.SKFluctuations.Hierarchy.diagonalPointSteps_congr line 529
  26. theorem OAI.SKFluctuations.Hierarchy.diagonalPointSteps_append line 540
  27. def OAI.SKFluctuations.Hierarchy.extendBoundary line 550
  28. theorem OAI.SKFluctuations.Hierarchy.extendBoundary_le line 553
  29. theorem OAI.SKFluctuations.Hierarchy.extendBoundary_gt line 556
  30. theorem OAI.SKFluctuations.Hierarchy.extendBoundary_monotone line 559
  31. theorem OAI.SKFluctuations.Hierarchy.diagonalRoot_append_one line 575
  32. def OAI.SKFluctuations.Hierarchy.rootBoundaryCost line 611
  33. theorem OAI.SKFluctuations.Hierarchy.diagonalRoot_comparison line 617