OAI/Probability/SKRatio/Calculus/TwoSpin.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKRatio.TwoSpin.polynomialSum line 11
  2. lemma OAI.SKRatio.TwoSpin.polynomialSum_bound line 14
  3. lemma OAI.SKRatio.TwoSpin.affine_factor line 32
  4. def OAI.SKRatio.TwoSpin.rationalCoefficient line 40
  5. def OAI.SKRatio.TwoSpin.leadingCoefficient line 45
  6. def OAI.SKRatio.TwoSpin.remainder0 line 48
  7. def OAI.SKRatio.TwoSpin.remainder1 line 65
  8. def OAI.SKRatio.TwoSpin.remainder2 line 87
  9. def OAI.SKRatio.TwoSpin.remainder3 line 113
  10. def OAI.SKRatio.TwoSpin.remainder4 line 136
  11. def OAI.SKRatio.TwoSpin.remainder5 line 151
  12. def OAI.SKRatio.TwoSpin.remainder line 157
  13. lemma OAI.SKRatio.TwoSpin.remainder_bound line 165
  14. lemma OAI.SKRatio.TwoSpin.numerator_certificate line 199
  15. lemma OAI.SKRatio.TwoSpin.rational_remainder line 211
  16. lemma OAI.SKRatio.TwoSpin.rational_remainder_bound line 224
  17. def OAI.SKRatio.TwoSpin.pairBaseMass line 243
  18. def OAI.SKRatio.TwoSpin.pairMean line 246
  19. lemma OAI.SKRatio.TwoSpin.pairMean_explicit line 249
  20. lemma OAI.SKRatio.TwoSpin.pairBaseMass_nonneg line 256
  21. lemma OAI.SKRatio.TwoSpin.pairMean_mono line 264
  22. lemma OAI.SKRatio.TwoSpin.pairMean_add line 272
  23. lemma OAI.SKRatio.TwoSpin.pairMean_sub line 276
  24. lemma OAI.SKRatio.TwoSpin.pairMean_mul line 280
  25. lemma OAI.SKRatio.TwoSpin.abs_pairMean_le line 284
  26. lemma OAI.SKRatio.TwoSpin.pair_gradient_mean line 295
  27. lemma OAI.SKRatio.TwoSpin.pair_gradient_square line 301
  28. lemma OAI.SKRatio.TwoSpin.pairMean_swap line 307
  29. lemma OAI.SKRatio.TwoSpin.pair_second_gradient_square line 312
  30. lemma OAI.SKRatio.TwoSpin.pair_factor_control line 317
  31. lemma OAI.SKRatio.TwoSpin.pair_square_factor_control line 327
  32. lemma OAI.SKRatio.TwoSpin.abs_mul_le_one_pair line 338
  33. def OAI.SKRatio.TwoSpin.pairDensity line 342
  34. def OAI.SKRatio.TwoSpin.pairInterMean line 345
  35. def OAI.SKRatio.TwoSpin.pairResidual line 348
  36. def OAI.SKRatio.TwoSpin.pairVariance line 351
  37. def OAI.SKRatio.TwoSpin.pairGrad₁ line 354
  38. def OAI.SKRatio.TwoSpin.pairGrad₂ line 356
  39. lemma OAI.SKRatio.TwoSpin.pairSign_abs line 358
  40. lemma OAI.SKRatio.TwoSpin.pairSign_sq line 360
  41. lemma OAI.SKRatio.TwoSpin.pairDenominator_pos line 362
  42. lemma OAI.SKRatio.TwoSpin.pair_variance_nonneg line 368
  43. lemma OAI.SKRatio.TwoSpin.pair_density_nonneg line 374
  44. lemma OAI.SKRatio.TwoSpin.pair_density_variance_lower line 379
  45. lemma OAI.SKRatio.TwoSpin.pair_energy_lower line 411
  46. lemma OAI.SKRatio.TwoSpin.pairInterMean_swap line 439
  47. lemma OAI.SKRatio.TwoSpin.pair_second_energy_lower line 450
  48. lemma OAI.SKRatio.TwoSpin.pairInterMean_add line 458
  49. lemma OAI.SKRatio.TwoSpin.pairInterMean_nonneg line 464
  50. def OAI.SKRatio.TwoSpin.pairConditionalMean line 471
  51. def OAI.SKRatio.TwoSpin.signedCoefficient line 474
  52. lemma OAI.SKRatio.TwoSpin.signedCoefficient_eq line 480
  53. lemma OAI.SKRatio.TwoSpin.leading_signs line 486
  54. lemma OAI.SKRatio.TwoSpin.signedCoefficient_remainder line 491
  55. lemma OAI.SKRatio.TwoSpin.pairMean_const line 503
  56. lemma OAI.SKRatio.TwoSpin.uniform_cross_gradient line 507
  57. lemma OAI.SKRatio.TwoSpin.abs_pairGrad_product line 513
  58. lemma OAI.SKRatio.TwoSpin.leading_lower line 538
  59. lemma OAI.SKRatio.TwoSpin.signed_mean_lower line 552
  60. def OAI.SKRatio.TwoSpin.pairPrefactor line 586
  61. lemma OAI.SKRatio.TwoSpin.residual_factorization line 589
  62. lemma OAI.SKRatio.TwoSpin.variance_factorization line 597
  63. lemma OAI.SKRatio.TwoSpin.signed_factorization line 606
  64. lemma OAI.SKRatio.TwoSpin.pairPrefactor_bounds line 634
  65. theorem OAI.SKRatio.TwoSpin.pair_cubic_signed_bound line 652