OAI/MeasureTheory/CompactFactors/Amenability.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EuclideanFiveColor.Amenable.shift line 14
  2. lemma OAI.EuclideanFiveColor.Amenable.shift_apply line 17
  3. structure OAI.EuclideanFiveColor.Amenable.Mean line 21

    Source documentation

    A normalized positive translation-invariant real functional.

    structure Mean where
…
  4. lemma OAI.EuclideanFiveColor.Amenable.Mean.mono line 30
  5. lemma OAI.EuclideanFiveColor.Amenable.Mean.abs_le line 34
  6. lemma OAI.EuclideanFiveColor.Amenable.Mean.exists_lt line 41
  7. def OAI.EuclideanFiveColor.Amenable.Mean.normFn line 50
  8. lemma OAI.EuclideanFiveColor.Amenable.Mean.normFn_apply line 54
  9. def OAI.EuclideanFiveColor.Amenable.Mean.pairing line 56
  10. lemma OAI.EuclideanFiveColor.Amenable.Mean.pairing_apply line 61
  11. lemma OAI.EuclideanFiveColor.Amenable.Mean.pairing_bound line 64
  12. def OAI.EuclideanFiveColor.Amenable.Mean.pairingMap line 73
  13. def OAI.EuclideanFiveColor.Amenable.Mean.vector line 86
  14. lemma OAI.EuclideanFiveColor.Amenable.Mean.vector_pair line 88
  15. lemma OAI.EuclideanFiveColor.Amenable.Mean.vector_norm_le line 91
  16. lemma OAI.EuclideanFiveColor.Amenable.Mean.vector_add line 96
  17. lemma OAI.EuclideanFiveColor.Amenable.Mean.vector_smul line 102
  18. lemma OAI.EuclideanFiveColor.Amenable.Mean.vector_shift line 108
  19. lemma OAI.EuclideanFiveColor.Amenable.Mean.vector_map line 113
  20. def OAI.EuclideanFiveColor.Amenable.Mean.squareNorm line 121
  21. lemma OAI.EuclideanFiveColor.Amenable.Mean.squareNorm_apply line 123
  22. lemma OAI.EuclideanFiveColor.Amenable.Mean.jensen line 126
  23. def OAI.EuclideanFiveColor.Amenable.Mean.cross line 152
  24. lemma OAI.EuclideanFiveColor.Amenable.Mean.cross_apply line 159
  25. lemma OAI.EuclideanFiveColor.Amenable.Mean.cross_comm line 162
  26. lemma OAI.EuclideanFiveColor.Amenable.Mean.squareNorm_add line 166
  27. lemma OAI.EuclideanFiveColor.Amenable.Mean.squareNorm_shift line 174
  28. def OAI.EuclideanFiveColor.Amenable.Mean.correlation line 178
  29. lemma OAI.EuclideanFiveColor.Amenable.Mean.correlation_apply line 189
  30. lemma OAI.EuclideanFiveColor.Amenable.Mean.correlation_add line 193
  31. lemma OAI.EuclideanFiveColor.Amenable.Mean.correlation_zero line 202
  32. lemma OAI.EuclideanFiveColor.Amenable.Mean.correlation_shift line 209
  33. theorem OAI.EuclideanFiveColor.Amenable.Mean.vector_eq_zero_of_correlation_nonpos line 221

    Source documentation

    Invariant-mean van der Corput: positivity and finite translates suffice. There is no exchange of iterated means.

    theorem vector_eq_zero_of_correlation_nonpos (V : G →ᵇ H)
    (hc : M.map (M.correlation V V) ≤ 0) : M.vector V = 0 := by
…
  34. def OAI.EuclideanFiveColor.Amenable.Mean.orbit line 282
  35. lemma OAI.EuclideanFiveColor.Amenable.Mean.orbit_apply line 287
  36. lemma OAI.EuclideanFiveColor.Amenable.Mean.vector_orbit_invariant line 289
  37. lemma OAI.EuclideanFiveColor.Amenable.Mean.vector_orbit_pair_fixed line 301
  38. theorem OAI.EuclideanFiveColor.Amenable.Mean.vector_orbit_eq_zero line 314

    Source documentation

    The mean ergodic projection criterion, valid for every positive invariant mean and without an assumption that the group has a distinguished generator.

    theorem vector_orbit_eq_zero (U : G → H ≃ₗᵢ[ℝ] H)
    (hU : ∀ g h v, U (g+h) v = U g (U h v)) (v : H)
    (hv : ∀ w, (∀ g, U g w = w) → inner ℝ v w = 0) :
    M.vector (orbit U v) = 0 := by
…

    Mentions: OAI.EuclideanFiveColor.Amenable.Mean.orbit

  39. def OAI.EuclideanFiveColor.Amenable.Koopman.linear line 333
  40. lemma OAI.EuclideanFiveColor.Amenable.Koopman.linear_add line 336
  41. lemma OAI.EuclideanFiveColor.Amenable.Koopman.linear_zero line 348
  42. def OAI.EuclideanFiveColor.Amenable.Koopman.action line 353
  43. lemma OAI.EuclideanFiveColor.Amenable.Koopman.action_apply line 357
  44. lemma OAI.EuclideanFiveColor.Amenable.Koopman.action_add line 359
  45. lemma OAI.EuclideanFiveColor.Amenable.Koopman.coe_action line 362
  46. lemma OAI.EuclideanFiveColor.Amenable.Koopman.ae_eq_const_of_fixed line 375
  47. lemma OAI.EuclideanFiveColor.Amenable.Koopman.inner_fixed_zero line 387
  48. theorem OAI.EuclideanFiveColor.Amenable.Koopman.vector_orbit_zero line 400