Main.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.ThompsonNonamenability.thompson_F_boundary_with_exact_constant line 16
theorem OAI.ThompsonNonamenability.thompson_F_boundary_constant_formula line 38
Source documentation
The displayed formula has no additional normalization or hidden factor.
```
theorem thompson_F_boundary_constant_formula (D : ℕ) :
    boundaryConstant Analytic.displacementLipschitzConstant (1 / 2) D =
      ((1 / 2 : ℝ) ^ 2 / Analytic.displacementLipschitzConstant ^ 2 -
        4 / (D : ℝ)) / (4 * (1 - 1 / (D : ℝ))) := rfl
```
Mentions: OAI.ThompsonNonamenability.boundaryConstant, OAI.ThompsonNonamenability.Analytic.displacementLipschitzConstant
theorem OAI.ThompsonNonamenability.thompson_F_uniform_boundary line 45
Source documentation
A fixed finite subset of the genuine PL group uniformly expands every nonempty finite subset, in the unnormalized symmetric-difference form.
```
theorem thompson_F_uniform_boundary :
    ∃ (S : Finset F) (b : ℝ), S.Nonempty ∧ 0 < b ∧
      ∀ A : Finset F, A.Nonempty →
        ∃ h ∈ S, b * (A.card : ℝ) ≤ ((leftTranslate h A ∆ A).card : ℝ) := by
…
```
Mentions: OAI.ThompsonNonamenability.F, OAI.ThompsonNonamenability.leftTranslate
theorem OAI.ThompsonNonamenability.thompson_F_not_amenable line 65
Source documentation
Standard Thompson F admits no positive normalized left-invariant mean on all bounded real functions. The carrier is identified with the ordinary finite-breakpoint dyadic PL homeomorphisms by F.standardPLEquiv.
```
theorem thompson_F_not_amenable : ¬ Nonempty (InvariantMean F) := by
…
```
Mentions: OAI.ThompsonNonamenability.InvariantMean, OAI.ThompsonNonamenability.F
theorem OAI.ThompsonNonamenability.thompson_F_nonamenable_composition line 69
Distinct definitions of this name: ComparatorChallenges/ThompsonNonamenability.lean:78 (same statement text; different proof or body). Qualify references as OAI.ThompsonNonamenability.thompson_F_nonamenable_composition@path.