OAI/Probability/SKRatio/Variational/ScalarCoherent.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKRatio.Scalar.a line 11
  2. def OAI.SKRatio.Scalar.l line 13
  3. def OAI.SKRatio.Scalar.G line 15
  4. def OAI.SKRatio.Scalar.R line 17
  5. lemma OAI.SKRatio.Scalar.l_eq line 19
  6. lemma OAI.SKRatio.Scalar.l_pos line 20
  7. lemma OAI.SKRatio.Scalar.a_nonneg line 21
  8. lemma OAI.SKRatio.Scalar.a_le_one line 22
  9. lemma OAI.SKRatio.Scalar.l_lower line 26
  10. lemma OAI.SKRatio.Scalar.R_nonneg line 29
  11. def OAI.SKRatio.Scalar.F line 31
  12. def OAI.SKRatio.Scalar.Uā‚€ line 35
  13. def OAI.SKRatio.Scalar.Uā‚ line 38
  14. lemma OAI.SKRatio.Scalar.multiplier_affine_v line 42
  15. lemma OAI.SKRatio.Scalar.memLp_F line 47
  16. lemma OAI.SKRatio.Scalar.integral_F_pairing line 55
  17. lemma OAI.SKRatio.Scalar.integral_mean_zero_multiplier line 87
  18. lemma OAI.SKRatio.Scalar.mean_field line 104
  19. lemma OAI.SKRatio.Scalar.sd_field line 106
  20. lemma OAI.SKRatio.Scalar.field_centered_covariance line 114
  21. lemma OAI.SKRatio.Scalar.centered_field_v_rank_bound line 125
  22. lemma OAI.SKRatio.Scalar.integrable_multiplier_translate_square line 144
  23. lemma OAI.SKRatio.Scalar.weighted_square_centered line 149
  24. lemma OAI.SKRatio.Scalar.weighted_square_floor line 179
  25. def OAI.SKRatio.Scalar.coherentUpper line 188
  26. lemma OAI.SKRatio.Scalar.coherent_le_upper line 194
  27. lemma OAI.SKRatio.Scalar.memLp_stein_v line 200
  28. theorem OAI.SKRatio.Scalar.coherent_full_expansion line 208
  29. theorem OAI.SKRatio.Scalar.coherent_two_dimensional line 235
  30. lemma OAI.SKRatio.Scalar.quadratic_slack_bound line 256
  31. theorem OAI.SKRatio.Scalar.coherent_bound_of_slacks line 268