OAI/GroupTheory/Thompson/FiniteCorrelationBoundary.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

From the actual recursive vectors and correlations to a boundary bound

This finite analytic bridge averages the pointwise displacement estimate and uses the exact correlation variance theorem. Its intermediate hypotheses are later supplied by the actual dyadic coloring and affine transports.

  1. theorem OAI.ThompsonNonamenability.finite_energy_of_variance line 28
  2. theorem OAI.ThompsonNonamenability.boundaryConstant_le_of_correlations line 56