OAI/MeasureTheory/CompactFactors/AlgebraModels.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.EuclideanFiveColor.BoundedMeasurable.covariance_sub_left line 39
  2. lemma OAI.EuclideanFiveColor.BoundedMeasurable.covariance_sub_right line 48
  3. lemma OAI.EuclideanFiveColor.BoundedMeasurable.covariance_norm_left line 59
  4. lemma OAI.EuclideanFiveColor.BoundedMeasurable.covariance_norm_right line 81
  5. lemma OAI.EuclideanFiveColor.BoundedMeasurable.meanNorm_zero_of_dense line 112
  6. lemma OAI.EuclideanFiveColor.BoundedMeasurable.covariance_zero_of_dense line 137
  7. lemma OAI.EuclideanFiveColor.RelativeProduct.graph_mixture line 164
  8. lemma OAI.EuclideanFiveColor.RelativeProduct.map_mixture line 178
  9. lemma OAI.EuclideanFiveColor.RelativeProduct.square_fiber line 189
  10. lemma OAI.EuclideanFiveColor.RelativeProduct.law_map_base line 196
  11. lemma OAI.EuclideanFiveColor.RelativeProduct.conditional_square line 200
  12. lemma OAI.EuclideanFiveColor.BoundedMeasurable.conditional_tensor line 221
  13. lemma OAI.EuclideanFiveColor.BoundedMeasurable.factor_preserving line 235
  14. lemma OAI.EuclideanFiveColor.BoundedMeasurable.covariance_tensor line 244
  15. lemma OAI.EuclideanFiveColor.BoundedMeasurable.covariance_tensor_mean_zero line 266
  16. inductive OAI.EuclideanFiveColor.BoundedMeasurable.FiniteTensor line 287
  17. lemma OAI.EuclideanFiveColor.BoundedMeasurable.FiniteTensor.zero line 291
  18. lemma OAI.EuclideanFiveColor.BoundedMeasurable.FiniteTensor.sum line 296
  19. lemma OAI.EuclideanFiveColor.BoundedMeasurable.func_sum_apply line 305
  20. def OAI.EuclideanFiveColor.BoundedMeasurable.codeCell line 315
  21. lemma OAI.EuclideanFiveColor.BoundedMeasurable.tensor_code_finite line 321
  22. lemma OAI.EuclideanFiveColor.BoundedMeasurable.finiteTensor_dense line 340
  23. lemma OAI.EuclideanFiveColor.BoundedMeasurable.pairVanishing_of_covariance line 368
  24. lemma OAI.EuclideanFiveColor.BoundedMeasurable.square_equivariant line 403
  25. lemma OAI.EuclideanFiveColor.BoundedMeasurable.covariance_finiteTensor_mean_zero line 412
  26. lemma OAI.EuclideanFiveColor.BoundedMeasurable.square_pairVanishing line 429
  27. lemma OAI.EuclideanFiveColor.BoundedMeasurable.square_tensor_centered line 456
  28. lemma OAI.EuclideanFiveColor.BoundedMeasurable.tensor_prod line 481
  29. lemma OAI.EuclideanFiveColor.BoundedMeasurable.centered_conditional_mean_zero line 492
  30. lemma OAI.EuclideanFiveColor.AlgebraReplacement.prod_sub_prod line 537
  31. lemma OAI.EuclideanFiveColor.BoundedMeasurable.Family.conditional_sum line 555
  32. lemma OAI.EuclideanFiveColor.BoundedMeasurable.conditional_multiple_mean_zero line 566
  33. def OAI.EuclideanFiveColor.BoundedMeasurable.scaleHom line 619
  34. lemma OAI.EuclideanFiveColor.BoundedMeasurable.scaleHom_apply line 620
  35. lemma OAI.EuclideanFiveColor.BoundedMeasurable.scaleHom_add line 621
  36. lemma OAI.EuclideanFiveColor.BoundedMeasurable.scaleHom_sub line 622
  37. lemma OAI.EuclideanFiveColor.BoundedMeasurable.shifted_admissible line 625
  38. lemma OAI.EuclideanFiveColor.BoundedMeasurable.conditional_integer_multiple_mean_zero line 652