OAI/Probability/SKFluctuations/ComparisonMinimumRealOverlapConclusion.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Comparison Minimum Real Overlap Conclusion.

  1. theorem OAI.SKFluctuations.comparison_minimum_retained_overlap_real_moment_normalized line 15
  2. theorem OAI.SKFluctuations.orderedOverlap_pow_gram line 131
  3. theorem OAI.SKFluctuations.levelPairMean_overlap_pow_monotone line 142
  4. theorem OAI.SKFluctuations.rootLevelPairMean_overlap_even_monotone line 161
  5. theorem OAI.SKFluctuations.physicalOverlapMoment_eq_rootLevelPairMean line 177
  6. theorem OAI.SKFluctuations.physicalOverlapMoment_mono line 191
  7. theorem OAI.SKFluctuations.physicalSpinMoment_mono line 212
  8. theorem OAI.SKFluctuations.Hierarchy.prefixContinuation_merge_same_mass line 250
  9. theorem OAI.SKFluctuations.Hierarchy.prefixTest_merge_same_mass line 260
  10. theorem OAI.SKFluctuations.Hierarchy.levelPairMean_after_same_mass line 273
  11. theorem OAI.SKFluctuations.Hierarchy.stepPowerDisorder_after_same_mass line 285
  12. theorem OAI.SKFluctuations.physicalOverlap_after_same_mass line 307
  13. theorem OAI.SKFluctuations.physicalOverlap_intermediate_same_mass_le line 322
  14. theorem OAI.SKFluctuations.physicalSpin_after_same_mass line 335
  15. theorem OAI.SKFluctuations.physicalSpin_intermediate_same_mass_le line 353