OAI/MeasureTheory/CompactFactors/BoundedFunctions.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EuclideanFiveColor.BoundedMeasurable.algebra line 13
  2. abbrev OAI.EuclideanFiveColor.BoundedMeasurable.Func line 27
  3. instance OAI.EuclideanFiveColor.BoundedMeasurable.(instance at line 29) line 29
  4. lemma OAI.EuclideanFiveColor.BoundedMeasurable.measurable line 31
  5. def OAI.EuclideanFiveColor.BoundedMeasurable.bound line 33
  6. lemma OAI.EuclideanFiveColor.BoundedMeasurable.norm_le_bound line 34
  7. lemma OAI.EuclideanFiveColor.BoundedMeasurable.ext line 36
  8. lemma OAI.EuclideanFiveColor.BoundedMeasurable.add_apply line 37
  9. lemma OAI.EuclideanFiveColor.BoundedMeasurable.mul_apply line 38
  10. lemma OAI.EuclideanFiveColor.BoundedMeasurable.sub_apply line 39
  11. lemma OAI.EuclideanFiveColor.BoundedMeasurable.zero_apply line 40
  12. lemma OAI.EuclideanFiveColor.BoundedMeasurable.one_apply line 41
  13. lemma OAI.EuclideanFiveColor.BoundedMeasurable.smul_apply line 42
  14. lemma OAI.EuclideanFiveColor.BoundedMeasurable.real_smul_apply line 43
  15. def OAI.EuclideanFiveColor.BoundedMeasurable.bmConj line 45
  16. lemma OAI.EuclideanFiveColor.BoundedMeasurable.conj_apply line 47
  17. def OAI.EuclideanFiveColor.BoundedMeasurable.comp line 49
  18. lemma OAI.EuclideanFiveColor.BoundedMeasurable.comp_apply line 51
  19. lemma OAI.EuclideanFiveColor.BoundedMeasurable.memLp line 56
  20. def OAI.EuclideanFiveColor.BoundedMeasurable.lp line 59
  21. lemma OAI.EuclideanFiveColor.BoundedMeasurable.coe_lp line 60
  22. lemma OAI.EuclideanFiveColor.BoundedMeasurable.lp_congr line 62
  23. lemma OAI.EuclideanFiveColor.BoundedMeasurable.lp_add line 65
  24. lemma OAI.EuclideanFiveColor.BoundedMeasurable.lp_smul line 68
  25. def OAI.EuclideanFiveColor.BoundedMeasurable.l2 line 70
  26. lemma OAI.EuclideanFiveColor.BoundedMeasurable.l2_ae line 75
  27. lemma OAI.EuclideanFiveColor.BoundedMeasurable.l2_eq_iff line 77
  28. lemma OAI.EuclideanFiveColor.BoundedMeasurable.integral_l2 line 83
  29. lemma OAI.EuclideanFiveColor.BoundedMeasurable.inner_l2 line 86
  30. lemma OAI.EuclideanFiveColor.BoundedMeasurable.l2_norm_mul_le line 93
  31. lemma OAI.EuclideanFiveColor.BoundedMeasurable.l2_norm_le line 100
  32. lemma OAI.EuclideanFiveColor.BoundedMeasurable.integrable line 113
  33. lemma OAI.EuclideanFiveColor.BoundedMeasurable.integrable_norm_sq line 116
  34. lemma OAI.EuclideanFiveColor.BoundedMeasurable.norm_l2_sq line 122
  35. def OAI.EuclideanFiveColor.BoundedMeasurable.expect line 127
  36. lemma OAI.EuclideanFiveColor.BoundedMeasurable.expect_apply line 133
  37. lemma OAI.EuclideanFiveColor.BoundedMeasurable.expect_bound line 136
  38. lemma OAI.EuclideanFiveColor.BoundedMeasurable.expect_add line 141
  39. lemma OAI.EuclideanFiveColor.BoundedMeasurable.expect_smul line 145
  40. def OAI.EuclideanFiveColor.BoundedMeasurable.expectLinear line 149
  41. lemma OAI.EuclideanFiveColor.BoundedMeasurable.expect_conj line 154
  42. abbrev OAI.EuclideanFiveColor.BoundedMeasurable.conditional line 161
  43. def OAI.EuclideanFiveColor.BoundedMeasurable.project line 163
  44. lemma OAI.EuclideanFiveColor.BoundedMeasurable.project_apply line 166
  45. lemma OAI.EuclideanFiveColor.BoundedMeasurable.conditional_integral line 171
  46. lemma OAI.EuclideanFiveColor.BoundedMeasurable.project_integral line 175
  47. lemma OAI.EuclideanFiveColor.BoundedMeasurable.conditional_pullout line 179
  48. lemma OAI.EuclideanFiveColor.BoundedMeasurable.conditional_lift line 187
  49. lemma OAI.EuclideanFiveColor.BoundedMeasurable.conditional_congr line 196
  50. lemma OAI.EuclideanFiveColor.BoundedMeasurable.conditional_norm_l2_le line 202
  51. lemma OAI.EuclideanFiveColor.BoundedMeasurable.project_eq_condexp line 215