OAI/MeasureTheory/CompactFactors/Separability.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.EuclideanFiveColor.Amenable.Mean.vector_real line 23
  2. lemma OAI.EuclideanFiveColor.Amenable.Mean.norm_mean_zero_of_square line 28
  3. lemma OAI.EuclideanFiveColor.BoundedMeasurable.l2_inner line 45
  4. lemma OAI.EuclideanFiveColor.BoundedMeasurable.inner_act line 53
  5. lemma OAI.EuclideanFiveColor.BoundedMeasurable.integral_act line 59
  6. lemma OAI.EuclideanFiveColor.BoundedMeasurable.l2_mul_norm_le line 62
  7. lemma OAI.EuclideanFiveColor.BoundedMeasurable.func_prod_apply line 89
  8. lemma OAI.EuclideanFiveColor.BoundedMeasurable.conj_conj line 95
  9. lemma OAI.EuclideanFiveColor.BoundedMeasurable.conj_mul line 96
  10. lemma OAI.EuclideanFiveColor.BoundedMeasurable.conj_prod line 97
  11. lemma OAI.EuclideanFiveColor.BoundedMeasurable.comp_prod line 100
  12. lemma OAI.EuclideanFiveColor.BoundedMeasurable.act_prod line 104
  13. lemma OAI.EuclideanFiveColor.BoundedMeasurable.act_zero line 106
  14. lemma OAI.EuclideanFiveColor.BoundedMeasurable.prod_orbit_correlation line 108
  15. lemma OAI.EuclideanFiveColor.BoundedMeasurable.prod_shift_erase line 116
  16. lemma OAI.EuclideanFiveColor.BoundedMeasurable.l2_inner_mul line 132
  17. lemma OAI.EuclideanFiveColor.BoundedMeasurable.correlation_product line 139
  18. lemma OAI.EuclideanFiveColor.BoundedMeasurable.norm_l2_conj line 166
  19. lemma OAI.EuclideanFiveColor.BoundedMeasurable.inner_replace_project line 170
  20. lemma OAI.EuclideanFiveColor.BoundedMeasurable.inner_project_bound line 186
  21. lemma OAI.EuclideanFiveColor.BoundedMeasurable.avg_project_bound line 198
  22. lemma OAI.EuclideanFiveColor.BoundedMeasurable.prod_act_project_lift line 213
  23. def OAI.EuclideanFiveColor.BoundedMeasurable.PairVanishing line 232
  24. lemma OAI.EuclideanFiveColor.BoundedMeasurable.pairVanishing_of_ergodic line 238
  25. def OAI.EuclideanFiveColor.BoundedMeasurable.Admissible line 247
  26. lemma OAI.EuclideanFiveColor.BoundedMeasurable.Admissible.erase_diff line 252
  27. theorem OAI.EuclideanFiveColor.BoundedMeasurable.avg_product_zero_of_pair line 268

    Source documentation

    Centered multiple vector averages for every invariant mean. The proof only uses the actual conditional pair criterion, never exchanges iterated means.

    theorem avg_product_zero_of_pair (M : Amenable.Mean G) (hpair : PairVanishing μ q hq M)
    (s : Finset ι) (φ : ι → G →+ G) (f : ι → Func X) (ha : Admissible s φ)
    (hc : ∃ j∈s, l2 μ (project μ q hq (f j)) = 0) :
    Family.avg μ M (∏ i∈s, Family.orbit (φ i) (f i)) = 0 := by
…

    Mentions: OAI.EuclideanFiveColor.Amenable.Mean, OAI.EuclideanFiveColor.BoundedMeasurable.PairVanishing, OAI.EuclideanFiveColor.BoundedMeasurable.Func, OAI.EuclideanFiveColor.BoundedMeasurable.Admissible, OAI.EuclideanFiveColor.BoundedMeasurable.l2, OAI.EuclideanFiveColor.BoundedMeasurable.project, OAI.EuclideanFiveColor.BoundedMeasurable.Family.avg, OAI.EuclideanFiveColor.BoundedMeasurable.Family.orbit

  28. def OAI.EuclideanFiveColor.BoundedMeasurable.Family.meanNorm line 367
  29. lemma OAI.EuclideanFiveColor.BoundedMeasurable.Family.meanNorm_nonneg line 368
  30. lemma OAI.EuclideanFiveColor.BoundedMeasurable.Family.meanNorm_mono line 372
  31. lemma OAI.EuclideanFiveColor.BoundedMeasurable.Family.meanNorm_congr line 374
  32. lemma OAI.EuclideanFiveColor.BoundedMeasurable.Family.meanNorm_le line 380
  33. lemma OAI.EuclideanFiveColor.BoundedMeasurable.Family.meanNorm_zero line 384
  34. lemma OAI.EuclideanFiveColor.BoundedMeasurable.Family.meanNorm_add_le line 390
  35. lemma OAI.EuclideanFiveColor.BoundedMeasurable.Family.meanNorm_neg line 398
  36. lemma OAI.EuclideanFiveColor.BoundedMeasurable.Family.meanNorm_sub_le line 404
  37. lemma OAI.EuclideanFiveColor.BoundedMeasurable.Family.meanNorm_mul_le line 410
  38. lemma OAI.EuclideanFiveColor.BoundedMeasurable.Family.meanNorm_const line 419
  39. lemma OAI.EuclideanFiveColor.BoundedMeasurable.Family.meanNorm_add_zero line 426
  40. lemma OAI.EuclideanFiveColor.BoundedMeasurable.Family.meanNorm_mul_zero line 431
  41. lemma OAI.EuclideanFiveColor.BoundedMeasurable.Family.meanNorm_sum_zero line 436
  42. lemma OAI.EuclideanFiveColor.BoundedMeasurable.Family.meanNorm_eq_zero_of_approx line 445
  43. def OAI.EuclideanFiveColor.BoundedMeasurable.Family.conditional line 469
  44. lemma OAI.EuclideanFiveColor.BoundedMeasurable.Family.conditional_apply line 473
  45. lemma OAI.EuclideanFiveColor.BoundedMeasurable.Family.conditional_add line 476
  46. lemma OAI.EuclideanFiveColor.BoundedMeasurable.Family.conditional_sub line 480
  47. def OAI.EuclideanFiveColor.BoundedMeasurable.covariance line 486
  48. lemma OAI.EuclideanFiveColor.BoundedMeasurable.covariance_apply line 490
  49. lemma OAI.EuclideanFiveColor.BoundedMeasurable.covariance_add_left line 495
  50. lemma OAI.EuclideanFiveColor.BoundedMeasurable.covariance_add_right line 508
  51. lemma OAI.EuclideanFiveColor.BoundedMeasurable.conditional_mul_project_act line 525
  52. lemma OAI.EuclideanFiveColor.BoundedMeasurable.covariance_center line 536
  53. lemma OAI.EuclideanFiveColor.BoundedMeasurable.covariance_mean_zero line 553