OAI/Probability/SKSupport/Regularity/ParameterChords.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ZeroTemperatureSK.OrderParameter.chord line 12
  2. lemma OAI.ZeroTemperatureSK.OrderParameter.chord_extend line 25
  3. lemma OAI.ZeroTemperatureSK.OrderParameter.chord_distance line 31
  4. lemma OAI.ZeroTemperatureSK.OrderParameter.chord_bound line 36
  5. def OAI.ZeroTemperatureSK.variationStep line 41
  6. lemma OAI.ZeroTemperatureSK.variationStep_pos line 42
  7. lemma OAI.ZeroTemperatureSK.variationStep_mem line 43
  8. lemma OAI.ZeroTemperatureSK.variationStep_limit line 48
  9. def OAI.ZeroTemperatureSK.perturbation line 52
  10. lemma OAI.ZeroTemperatureSK.perturbation_diff line 54
  11. lemma OAI.ZeroTemperatureSK.perturbation_distance_limit line 58
  12. lemma OAI.ZeroTemperatureSK.finiteCoeff_offset line 74
  13. def OAI.ZeroTemperatureSK.positiveCoeff line 97
  14. def OAI.ZeroTemperatureSK.positiveGamma line 100
  15. def OAI.ZeroTemperatureSK.positiveTerminal line 103
  16. lemma OAI.ZeroTemperatureSK.positiveCoeff_pos line 106
  17. lemma OAI.ZeroTemperatureSK.positiveCoeff_monotone line 110
  18. lemma OAI.ZeroTemperatureSK.positiveCoeff_bound line 119
  19. lemma OAI.ZeroTemperatureSK.positiveTerminal_pos line 126
  20. lemma OAI.ZeroTemperatureSK.positiveGamma_eq line 129
  21. lemma OAI.ZeroTemperatureSK.positiveGamma_intervalIntegrable line 135
  22. lemma OAI.ZeroTemperatureSK.positiveGamma_L1_bound line 138
  23. lemma OAI.ZeroTemperatureSK.positiveGamma_L1 line 154
  24. lemma OAI.ZeroTemperatureSK.positiveGamma_bound line 160
  25. lemma OAI.ZeroTemperatureSK.positiveTerminal_inv_tendsto line 169