OAI/Probability/SKRatio/Gaussian/PlantedCriterion.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKRatio.Planted.continuous_field line 17
  2. lemma OAI.SKRatio.Planted.continuous_mean line 22
  3. lemma OAI.SKRatio.Planted.continuous_conditionalVariance line 27
  4. lemma OAI.SKRatio.Planted.continuous_gradientWeight line 32
  5. lemma OAI.SKRatio.Planted.continuous_gradientForm line 37
  6. def OAI.SKRatio.Planted.formBad line 61
  7. lemma OAI.SKRatio.Planted.formBad_measurable line 64
  8. lemma OAI.SKRatio.Planted.gradientForm_smul line 72
  9. lemma OAI.SKRatio.Planted.gradientForm_zero line 94
  10. lemma OAI.SKRatio.Planted.formBad_iff_unit line 97
  11. lemma OAI.SKRatio.Planted.gradient_drift_of_form_good line 131
  12. lemma OAI.SKRatio.Planted.gradient_drift_rough line 151
  13. theorem OAI.SKRatio.Planted.ratio_cutoff_of_planted_form line 168