OAI/GroupTheory/Thompson/FiniteCoarea.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ThompsonNonamenability.sum_indicator_eq_card line 17
2. theorem OAI.ThompsonNonamenability.sum_abs_indicators_eq_card_symmDiff line 27
3. theorem OAI.ThompsonNonamenability.finite_value_mem line 46
4. def OAI.ThompsonNonamenability.FiniteLevelChain.levelSet line 60

   Source documentation

   The strict superlevel set at the lower endpoint of a positive layer.

   def levelSet (c : FiniteLevelChain K p) (i : Fin c.n) : Finset G := by
   …

   Mentions: OAI.ThompsonNonamenability.FiniteLevelChain

5. theorem OAI.ThompsonNonamenability.FiniteLevelChain.levelSet_subset line 65
6. theorem OAI.ThompsonNonamenability.FiniteLevelChain.mem_levelSet line 69

   Source documentation

   The finite carrier restriction does not change positive-threshold membership.

   theorem mem_levelSet (c : FiniteLevelChain K p)
       (hpK : ∀ x, x ∉ K → p x = 0) (i : Fin c.n) (x : G) :
       x ∈ c.levelSet i ↔ c.value i.castSucc < p x := by
   …

   Mentions: OAI.ThompsonNonamenability.FiniteLevelChain

7. theorem OAI.ThompsonNonamenability.FiniteLevelChain.levelSet_nonempty line 87
8. theorem OAI.ThompsonNonamenability.FiniteLevelChain.coarea_mass line 109

   Source documentation

   Exact finite layer-cake identity for the mass.

   theorem coarea_mass (c : FiniteLevelChain K p)
       (hpK : ∀ x, x ∉ K → p x = 0) :
       (∑ x ∈ K, p x) =
         ∑ i : Fin c.n, c.gap i * ((c.levelSet i).card : ℝ) := by
   …

   Mentions: OAI.ThompsonNonamenability.FiniteLevelChain

9. theorem OAI.ThompsonNonamenability.mem_leftTranslate_iff line 141
10. theorem OAI.ThompsonNonamenability.FiniteLevelChain.coarea_translation line 155

    Source documentation

    Exact coarea identity for one left translation, over its finite support carrier.

    theorem coarea_translation (c : FiniteLevelChain K p)
        (hpK : ∀ x, x ∉ K → p x = 0) (h : G) :
        (∑ x ∈ K ∪ leftTranslate h K, |p (h⁻¹ * x) - p x|) =
          ∑ i : Fin c.n, c.gap i *
            ((leftTranslate h (c.levelSet i) ∆ c.levelSet i).card : ℝ) := by
    …

    Mentions: OAI.ThompsonNonamenability.FiniteLevelChain, OAI.ThompsonNonamenability.leftTranslate

11. theorem OAI.ThompsonNonamenability.FiniteLevelChain.coarea_sum line 196

    Source documentation

    Summing the exact translation identities introduces no cardinality factor.

    theorem coarea_sum (c : FiniteLevelChain K p)
        (hpK : ∀ x, x ∉ K → p x = 0) (S : Finset G) :
        (∑ h ∈ S, ∑ x ∈ K ∪ leftTranslate h K, |p (h⁻¹ * x) - p x|) =
          ∑ i : Fin c.n, c.gap i *
            (∑ h ∈ S, ((leftTranslate h (c.levelSet i) ∆ c.levelSet i).card : ℝ)) := by
    …

    Mentions: OAI.ThompsonNonamenability.FiniteLevelChain, OAI.ThompsonNonamenability.leftTranslate

12. theorem OAI.ThompsonNonamenability.finite_folner_of_small_defect_subset line 212

    Source documentation

    A nonempty level inside the supplied finite support has small total boundary.

    theorem finite_folner_of_small_defect_subset
        {K S : Finset G} {p : G → ℝ} {ε : ℝ}
        (hp0 : ∀ g, 0 ≤ p g)
        (hpK : ∀ g, g ∉ K → p g = 0)
        (mass : ∑ g ∈ K, p g = 1)
        (hdef : (∑ h ∈ S, ∑ x ∈ K ∪ leftTranslate h K,
          |p (h⁻¹ * x) - p x|) < ε) :
        ∃ A : Finset G, A ⊆ K ∧ A.Nonempty ∧
          (∑ h ∈ S, ((leftTranslate h A ∆ A).card : ℝ)) < ε * (A.card : ℝ) := by
    …

    Mentions: OAI.ThompsonNonamenability.mass, OAI.ThompsonNonamenability.leftTranslate

13. theorem OAI.ThompsonNonamenability.finite_folner_of_small_defect line 252

    Source documentation

    Finite probability with small total translation defect yields a finite Følner set.

    theorem finite_folner_of_small_defect
        {K S : Finset G} {p : G → ℝ} {ε : ℝ}
        (hp0 : ∀ g, 0 ≤ p g)
        (hpK : ∀ g, g ∉ K → p g = 0)
        (mass : ∑ g ∈ K, p g = 1)
        (hdef : (∑ h ∈ S, ∑ x ∈ K ∪ leftTranslate h K,
          |p (h⁻¹ * x) - p x|) < ε) :
        ∃ A : Finset G, A.Nonempty ∧
          (∑ h ∈ S, ((leftTranslate h A ∆ A).card : ℝ)) < ε * (A.card : ℝ) := by
    …

    Mentions: OAI.ThompsonNonamenability.mass, OAI.ThompsonNonamenability.leftTranslate