OAI/Probability/SKRatio/Calculus/PlusSpin.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKRatio.Calculus.field_replace_self line 12
  2. lemma OAI.SKRatio.Calculus.halfDiff_mean_self line 21
  3. def OAI.SKRatio.Calculus.plusSpin line 25
  4. theorem OAI.SKRatio.Calculus.pointwise_gradient_identity line 27
  5. lemma OAI.SKRatio.Calculus.hasDerivAt_tanh line 56
  6. lemma OAI.SKRatio.Calculus.tanh_lipschitz_abs line 63
  7. lemma OAI.SKRatio.Calculus.abs_tanh_le_abs line 71
  8. lemma OAI.SKRatio.Calculus.tanh_cubic_error line 74
  9. def OAI.SKRatio.Calculus.scalarVariance line 94
  10. lemma OAI.SKRatio.Calculus.scalarVariance_pos line 96
  11. lemma OAI.SKRatio.Calculus.scalarVariance_eq line 99
  12. lemma OAI.SKRatio.Calculus.tanh_difference_eq line 106
  13. lemma OAI.SKRatio.Calculus.normalized_tanh_difference line 111
  14. def OAI.SKRatio.Calculus.q line 124
  15. lemma OAI.SKRatio.Calculus.tanh_difference_variance line 126
  16. lemma OAI.SKRatio.Calculus.q_denominator line 135
  17. lemma OAI.SKRatio.Calculus.q_linear_bound line 143
  18. lemma OAI.SKRatio.Calculus.q_expansion line 152
  19. lemma OAI.SKRatio.Calculus.q_cubic_bound line 162
  20. lemma OAI.SKRatio.Calculus.q_quadratic_bound line 212
  21. lemma OAI.SKRatio.Calculus.field_flip_coordinate line 226
  22. def OAI.SKRatio.Calculus.conditionalVariance line 232
  23. lemma OAI.SKRatio.Calculus.conditionalVariance_pos line 235
  24. lemma OAI.SKRatio.Calculus.conditionalVariance_le_one line 238
  25. lemma OAI.SKRatio.Calculus.mean_abs_le_one line 243
  26. lemma OAI.SKRatio.Calculus.gradientWeight_pos line 246
  27. lemma OAI.SKRatio.Calculus.mean_weight_plus line 256
  28. lemma OAI.SKRatio.Calculus.halfDiff_mean_plus line 260
  29. lemma OAI.SKRatio.Calculus.variance_over_weight line 270
  30. lemma OAI.SKRatio.Calculus.pair_denominator_control line 280
  31. lemma OAI.SKRatio.Calculus.scalar_pair_denominator_control line 293
  32. lemma OAI.SKRatio.Calculus.complete_pair_square line 305
  33. lemma OAI.SKRatio.Calculus.weighted_pair_abs_le line 310
  34. lemma OAI.SKRatio.Calculus.pair_q_error line 322
  35. lemma OAI.SKRatio.Calculus.pair_square_replacement line 354
  36. def OAI.SKRatio.Calculus.pairSum line 381
  37. lemma OAI.SKRatio.Calculus.sum_transpose_triangle line 384
  38. lemma OAI.SKRatio.Calculus.sum_offdiag_pairs line 390
  39. lemma OAI.SKRatio.Calculus.pairSum_add line 411