BoundaryAlgebra.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The exact positive constant in the finite boundary obstruction

The energy inequality is rearranged only after proving the denominators positive. No sign condition is imposed on a correlation or on its error bound. The choice of the integer parameter is independent of the finite group set.

def OAI.ThompsonNonamenability.boundaryConstant line 19
theorem OAI.ThompsonNonamenability.boundary_denominator_pos line 22
theorem OAI.ThompsonNonamenability.boundary_numerator_pos line 29
theorem OAI.ThompsonNonamenability.boundaryConstant_pos line 43

theorem OAI.ThompsonNonamenability.boundaryConstant_le_of_energy line 52

Source documentation

Algebraic consequence of the genuine finite energy estimate.

theorem boundaryConstant_le_of_energy {L δ η : ℝ} {D : ℕ}
    (hL : 0 < L) (hD : 2 ≤ D)
    (henergy : δ ^ 2 ≤ L ^ 2 *
      (4 / (D : ℝ) + 4 * (1 - 1 / (D : ℝ)) * η)) :
    boundaryConstant L δ D ≤ η := by
…

Mentions: OAI.ThompsonNonamenability.boundaryConstant

theorem OAI.ThompsonNonamenability.exists_branching_parameter line 67
Source documentation
Choose the finite branching parameter before choosing any finite group set.
```
theorem exists_branching_parameter (L δ : ℝ) :
    ∃ D : ℕ, 2 ≤ D ∧ 4 * L ^ 2 / δ ^ 2 < (D : ℝ) := by
…
```