OAI/Probability/SKRatio/Calculus/RowControl.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKRatio.Calculus.pairSum_sub line 13
  2. lemma OAI.SKRatio.Calculus.pairSum_mul line 17
  3. lemma OAI.SKRatio.Calculus.pairSum_le line 21
  4. def OAI.SKRatio.Calculus.rowControl line 29
  5. lemma OAI.SKRatio.Calculus.rowControl_nonneg line 32
  6. lemma OAI.SKRatio.Calculus.row_le_rowControl line 35
  7. abbrev OAI.SKRatio.Calculus.R2 line 41
  8. abbrev OAI.SKRatio.Calculus.R3 line 42
  9. lemma OAI.SKRatio.Calculus.pair_row_bound line 44
  10. lemma OAI.SKRatio.Calculus.offdiag_abs_row_bound line 66
  11. lemma OAI.SKRatio.Calculus.eliminate_second_differences line 78
  12. def OAI.SKRatio.Calculus.gradientForm line 92
  13. lemma OAI.SKRatio.Calculus.field_difference_error line 102
  14. lemma OAI.SKRatio.Calculus.linear_field_replacement line 121
  15. lemma OAI.SKRatio.Calculus.completed_squares_replacement line 154
  16. theorem OAI.SKRatio.Calculus.pointwise_gradient_bound_plus line 188
  17. def OAI.SKRatio.Calculus.signProduct line 212
  18. lemma OAI.SKRatio.Calculus.signProduct_plus line 215
  19. lemma OAI.SKRatio.Calculus.plus_signProduct line 219
  20. lemma OAI.SKRatio.Calculus.signProduct_involutive line 223
  21. lemma OAI.SKRatio.Calculus.spin_signProduct line 228
  22. lemma OAI.SKRatio.Calculus.abs_spin line 232
  23. lemma OAI.SKRatio.Calculus.signProduct_replace line 235
  24. def OAI.SKRatio.Calculus.signConjugate line 242
  25. def OAI.SKRatio.Calculus.signPullback line 245
  26. lemma OAI.SKRatio.Calculus.halfDiff_signPullback line 248
  27. lemma OAI.SKRatio.Calculus.field_signConjugate line 255
  28. lemma OAI.SKRatio.Calculus.mean_signConjugate line 262
  29. lemma OAI.SKRatio.Calculus.generator_signConjugate line 268
  30. lemma OAI.SKRatio.Calculus.unweightedGradient_signPullback line 277
  31. lemma OAI.SKRatio.Calculus.gradient_drift_signPullback line 282
  32. lemma OAI.SKRatio.Calculus.signConjugate_symm line 292
  33. lemma OAI.SKRatio.Calculus.signConjugate_diag line 298
  34. lemma OAI.SKRatio.Calculus.abs_signConjugate line 302
  35. lemma OAI.SKRatio.Calculus.rowControl_signConjugate line 306
  36. lemma OAI.SKRatio.Calculus.instantaneous_gradient_bound_plus line 313
  37. theorem OAI.SKRatio.Calculus.pointwise_gradient_local_bound line 324
  38. def OAI.SKRatio.Calculus.euclideanOpNorm line 342
  39. lemma OAI.SKRatio.Calculus.euclideanOpNorm_nonneg line 344
  40. lemma OAI.SKRatio.Calculus.euclideanNorm_variance_le line 347
  41. lemma OAI.SKRatio.Calculus.gradientForm_linear_bound line 360
  42. lemma OAI.SKRatio.Calculus.abs_mean_variance_bound line 393
  43. lemma OAI.SKRatio.Calculus.mean_variance_bound line 405
  44. lemma OAI.SKRatio.Calculus.gradientForm_quadratic_bound line 409