OAI/Probability/SKGap/Terminal/PairCrossIdentity.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKGap.pairDensity line 13
  2. def OAI.SKGap.pairInterMean line 15
  3. def OAI.SKGap.pairResidual line 17
  4. def OAI.SKGap.pairVariance line 19
  5. def OAI.SKGap.pairGrad₁ line 22
  6. def OAI.SKGap.pairGrad₂ line 23
  7. lemma OAI.SKGap.pairSign_abs line 25
  8. lemma OAI.SKGap.pairSign_sq line 26
  9. lemma OAI.SKGap.pairDenominator_pos line 28
  10. lemma OAI.SKGap.reciprocal_affine line 34
  11. lemma OAI.SKGap.pair_gradient_reciprocal line 49
  12. lemma OAI.SKGap.pair_cross_coefficient_identity line 65
  13. lemma OAI.SKGap.pair_cross_pointwise line 87
  14. lemma OAI.SKGap.pair_cross_exact line 108
  15. lemma OAI.SKGap.pair_variance_nonneg line 146
  16. lemma OAI.SKGap.pair_density_nonneg line 152
  17. lemma OAI.SKGap.pair_variance_product line 157
  18. lemma OAI.SKGap.pair_weighted_product line 164
  19. lemma OAI.SKGap.pair_abs_weighted_product line 178
  20. lemma OAI.SKGap.pair_weighted_error line 196
  21. lemma OAI.SKGap.pair_abs_cost_lower line 216
  22. lemma OAI.SKGap.pair_density_variance_lower line 235