OAI/Probability/SKSupport/Density/SampleJets.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ZeroTemperatureSK.positivePath_sample_limit line 16
  2. def OAI.ZeroTemperatureSK.sampleJet line 29
  3. def OAI.ZeroTemperatureSK.actualJet line 32
  4. lemma OAI.ZeroTemperatureSK.sampleJet_limit line 35
  5. lemma OAI.ZeroTemperatureSK.sampleJet_measurable line 49
  6. lemma OAI.ZeroTemperatureSK.sampleJet_bound line 54
  7. def OAI.ZeroTemperatureSK.sampleQuartic line 71
  8. def OAI.ZeroTemperatureSK.sampleCoercive line 74
  9. lemma OAI.ZeroTemperatureSK.sample_coercivity line 78
  10. lemma OAI.ZeroTemperatureSK.sampleQuartic_integral_limit line 90
  11. lemma OAI.ZeroTemperatureSK.sampleCoercive_integral_limit line 108
  12. theorem OAI.ZeroTemperatureSK.actual_coercivity line 135