OAI/Probability/SKSupport/Density/CoerciveMoments.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ZeroTemperatureSK.coerciveJetPolynomial line 15
  2. def OAI.ZeroTemperatureSK.quarticJetPolynomial line 17
  3. lemma OAI.ZeroTemperatureSK.quarticMoment_scaled line 19
  4. lemma OAI.ZeroTemperatureSK.coercivePolynomial_scaled line 27
  5. lemma OAI.ZeroTemperatureSK.quarticJetPolynomial_bound line 37
  6. lemma OAI.ZeroTemperatureSK.coerciveJetPolynomial_bound line 43
  7. def OAI.ZeroTemperatureSK.sampleIndex line 74
  8. def OAI.ZeroTemperatureSK.sampleNNTime line 76
  9. lemma OAI.ZeroTemperatureSK.sampleIndex_lt line 78
  10. lemma OAI.ZeroTemperatureSK.sampleNNTime_le line 83
  11. lemma OAI.ZeroTemperatureSK.sampleNNTime_lower line 88
  12. def OAI.ZeroTemperatureSK.sampleTime line 95
  13. lemma OAI.ZeroTemperatureSK.sampleTime_limit line 98
  14. lemma OAI.ZeroTemperatureSK.sampleNNTime_limit line 105
  15. lemma OAI.ZeroTemperatureSK.sampleIndex_pos_eventually line 109
  16. lemma OAI.ZeroTemperatureSK.positiveCoeff_sample_eq line 114
  17. lemma OAI.ZeroTemperatureSK.positiveCoeff_sample_limit line 120
  18. lemma OAI.ZeroTemperatureSK.positiveCoeff_sample_bound line 125
  19. lemma OAI.ZeroTemperatureSK.positiveValue_sample line 133