OAI/Probability/SKRatio/Variational/FormAlgebra.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKRatio.Planted.quadratic line 16
  2. def OAI.SKRatio.Planted.weightedForm line 19
  3. def OAI.SKRatio.Planted.diagonalForm line 23
  4. def OAI.SKRatio.Planted.varianceKernel line 27
  5. def OAI.SKRatio.Planted.meanVarianceKernel line 28
  6. lemma OAI.SKRatio.Planted.continuous_varianceKernel line 31
  7. lemma OAI.SKRatio.Planted.continuous_meanVarianceKernel line 33
  8. def OAI.SKRatio.Planted.compactForm line 38
  9. lemma OAI.SKRatio.Planted.quadratic_add line 44
  10. lemma OAI.SKRatio.Planted.quadratic_sub line 47
  11. lemma OAI.SKRatio.Planted.quadratic_const_mul line 50
  12. lemma OAI.SKRatio.Planted.quadratic_inner line 54
  13. lemma OAI.SKRatio.Planted.quadratic_abs_le line 65
  14. lemma OAI.SKRatio.Planted.weightedForm_sub line 78
  15. lemma OAI.SKRatio.Planted.diagonalForm_sub line 83
  16. lemma OAI.SKRatio.Planted.diagonalForm_abs_le line 88
  17. lemma OAI.SKRatio.Planted.sum_offdiag_eq_full line 99
  18. lemma OAI.SKRatio.Planted.gradient_pair_expansion line 105
  19. theorem OAI.SKRatio.Planted.gradientForm_eq_compactForm line 125