OAI/GroupTheory/Thompson/FiniteAverage.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Real finite averages and left-translation cancellation

These are literal finite sums. The translation estimate cancels the common intersection of the two finite sets, and the function bound is global. No invariant mean, support assumption, or limiting average is used.

  1. def OAI.ThompsonNonamenability.realAvg line 28
  2. theorem OAI.ThompsonNonamenability.realAvg_eq_sum_div line 31
  3. theorem OAI.ThompsonNonamenability.realAvg_congr line 35
  4. theorem OAI.ThompsonNonamenability.realAvg_zero line 40
  5. theorem OAI.ThompsonNonamenability.realAvg_add line 43
  6. theorem OAI.ThompsonNonamenability.realAvg_sub line 47
  7. theorem OAI.ThompsonNonamenability.realAvg_neg line 51
  8. theorem OAI.ThompsonNonamenability.realAvg_const_mul line 55
  9. theorem OAI.ThompsonNonamenability.realAvg_mul_const line 59
  10. theorem OAI.ThompsonNonamenability.realAvg_sum line 63
  11. theorem OAI.ThompsonNonamenability.realAvg_sum_univ line 68
  12. theorem OAI.ThompsonNonamenability.realAvg_mono line 72
  13. theorem OAI.ThompsonNonamenability.realAvg_nonneg line 77
  14. theorem OAI.ThompsonNonamenability.realAvg_const line 81
  15. theorem OAI.ThompsonNonamenability.realAvg_le_const line 86
  16. theorem OAI.ThompsonNonamenability.const_le_realAvg line 90
  17. theorem OAI.ThompsonNonamenability.abs_realAvg_le line 94
  18. theorem OAI.ThompsonNonamenability.realAvg_abs_le_one line 101
  19. theorem OAI.ThompsonNonamenability.sum_sub_eq_sdiff_sub line 110

    Source documentation

    The exact common-intersection cancellation, before any estimate.

    theorem sum_sub_eq_sdiff_sub (U V : Finset α) (f : α → ℝ) :
    (∑ x ∈ U, f x) - ∑ x ∈ V, f x =
      (∑ x ∈ U \ V, f x) - ∑ x ∈ V \ U, f x :=
…
  20. theorem OAI.ThompsonNonamenability.card_symmDiff_eq_sdiff_add line 115
  21. theorem OAI.ThompsonNonamenability.abs_sum_le_card line 121
  22. theorem OAI.ThompsonNonamenability.abs_sum_sub_le_card_symmDiff line 129

    Source documentation

    The full symmetric difference counts both residual pieces exactly once.

    theorem abs_sum_sub_le_card_symmDiff (U V : Finset α) (f : α → ℝ)
    (hf : ∀ x, |f x| ≤ 1) :
    |(∑ x ∈ U, f x) - ∑ x ∈ V, f x| ≤ ((U ∆ V).card : ℝ) := by
…
  23. def OAI.ThompsonNonamenability.leftTranslate line 148
  24. def OAI.ThompsonNonamenability.boundaryRatio line 150
  25. theorem OAI.ThompsonNonamenability.sum_leftTranslate line 153
  26. theorem OAI.ThompsonNonamenability.card_leftTranslate line 158
  27. theorem OAI.ThompsonNonamenability.boundaryRatio_nonneg line 162
  28. theorem OAI.ThompsonNonamenability.abs_sum_translate_sub_le line 165
  29. theorem OAI.ThompsonNonamenability.abs_realAvg_translate_sub_le line 173

    Source documentation

    The finite-translation inequality for every globally unit-bounded function.

    theorem abs_realAvg_translate_sub_le (A : Finset G) (hA : A.Nonempty)
    (h : G) (f : G → ℝ) (hf : ∀ g, |f g| ≤ 1) :
    |realAvg A (fun g => f (h * g)) - realAvg A f| ≤ boundaryRatio A h := by
…

    Mentions: OAI.ThompsonNonamenability.realAvg, OAI.ThompsonNonamenability.boundaryRatio

  30. def OAI.ThompsonNonamenability.boundaryMax line 181

    Source documentation

    The real maximum requires an actual member of the fixed transport set.

    def boundaryMax (S : Finset G) (hS : S.Nonempty) (A : Finset G) : ℝ := by
…
  31. theorem OAI.ThompsonNonamenability.boundaryMax_attained line 185
  32. theorem OAI.ThompsonNonamenability.boundaryRatio_le_max line 192
  33. theorem OAI.ThompsonNonamenability.boundaryMax_nonneg line 198
  34. theorem OAI.ThompsonNonamenability.exists_boundary_ge_of_le_max line 204