OAI/Probability/SKGap/Stability/LawMean.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKGapCutoff.lawMean line 161
  2. def OAI.SKGapCutoff.lawVariance line 164
  3. def OAI.SKGapCutoff.pushLaw line 167
  4. lemma OAI.SKGapCutoff.lawMean_pushLaw line 171
  5. lemma OAI.SKGapCutoff.lawMean_const line 179
  6. lemma OAI.SKGapCutoff.lawMean_mono line 182
  7. lemma OAI.SKGapCutoff.lawMean_le_const line 186
  8. lemma OAI.SKGapCutoff.lawMean_add line 190
  9. lemma OAI.SKGapCutoff.lawMean_sub line 194
  10. lemma OAI.SKGapCutoff.lawMean_smul line 198
  11. lemma OAI.SKGapCutoff.lawVariance_centered line 202
  12. lemma OAI.SKGapCutoff.lawVariance_sub_const line 214
  13. lemma OAI.SKGapCutoff.pushLaw_sum line 225
  14. lemma OAI.SKGapCutoff.pushLaw_nonneg line 231
  15. lemma OAI.SKGapCutoff.evolvedLaw_variance_decomposition line 239
  16. theorem OAI.SKGapCutoff.trajectory_variance_from_gradient line 251
  17. lemma OAI.SKGapCutoff.pushed_totalVariation_le_worst line 267
  18. def OAI.SKGapCutoff.preparationLaw line 280
  19. lemma OAI.SKGapCutoff.lawMean_preparationLaw line 284
  20. lemma OAI.SKGapCutoff.preparationLaw_nonneg line 289
  21. lemma OAI.SKGapCutoff.preparationLaw_sum line 295
  22. lemma OAI.SKGapCutoff.preparationLaw_poincare line 300
  23. def OAI.SKGapCutoff.lawBarycenter line 317
  24. lemma OAI.SKGapCutoff.lawMean_inner_sub line 320
  25. theorem OAI.SKGapCutoff.worstContinuous_lower_from_prepared_image line 326
  26. lemma OAI.SKGapCutoff.preparationFlow_zero line 384
  27. lemma OAI.SKGapCutoff.pushLaw_gibbs line 393
  28. lemma OAI.SKGapCutoff.preparationLaw_zero line 401
  29. lemma OAI.SKGapCutoff.polynomial_signal_error line 406