OAI/Probability/SKFluctuations/ComparisonMinimumMassCenter.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Comparison Minimum Mass Center.

  1. theorem OAI.SKFluctuations.comparison_minimum_mass_center line 15
  2. theorem OAI.SKFluctuations.inverseConstraint_mass_mem line 114
  3. theorem OAI.SKFluctuations.constrainedCoefficient_inverse line 121
  4. theorem OAI.SKFluctuations.changedField_radius_growth line 134
  5. theorem OAI.SKFluctuations.changedField_toNNReal_radius_growth line 162
  6. theorem OAI.SKFluctuations.hasDerivAt_comparisonStrength line 204
  7. theorem OAI.SKFluctuations.comparisonLogSlope_strength line 213
  8. theorem OAI.SKFluctuations.strength_radial_monotonicities line 224
  9. def OAI.SKFluctuations.Hierarchy.pathTailTest line 272
  10. theorem OAI.SKFluctuations.Hierarchy.pathTailTest_measurable line 282
  11. theorem OAI.SKFluctuations.Hierarchy.pathTailTest_abs_le line 293
  12. theorem OAI.SKFluctuations.Hierarchy.pathTailTest_integrable line 303
  13. theorem OAI.SKFluctuations.Hierarchy.integral_pathTailTest line 319
  14. def OAI.SKFluctuations.Hierarchy.pathLayerEnergy line 358
  15. theorem OAI.SKFluctuations.Hierarchy.pathLayerEnergy_measurable line 368
  16. theorem OAI.SKFluctuations.Hierarchy.pathLayerEnergy_bounded line 395
  17. theorem OAI.SKFluctuations.Hierarchy.pathLayerEnergy_integrable line 430
  18. theorem OAI.SKFluctuations.Hierarchy.integral_pathLayerEnergy_nil line 443
  19. theorem OAI.SKFluctuations.Hierarchy.integral_pathLayerEnergy line 472
  20. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchyHessian_le_physical_layers line 505
  21. def OAI.SKFluctuations.Hierarchy.layerCutSchedule line 527
  22. def OAI.SKFluctuations.Hierarchy.weightedPathIncrements line 532
  23. theorem OAI.SKFluctuations.Hierarchy.weightedPathIncrements_shift line 536
  24. theorem OAI.SKFluctuations.Hierarchy.hierarchyMeanPath_source line 548
  25. theorem OAI.SKFluctuations.Hierarchy.pathTailTest_meanPath line 566
  26. theorem OAI.SKFluctuations.Hierarchy.pathTailTest_weightedPathIncrements line 582
  27. theorem OAI.SKFluctuations.Hierarchy.pathLayerEnergy_eq_weightedPathIncrements line 595