PublishedInputs.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Haar concentration and Gaussian Poincaré inequalities.

Gromov–Milman, A topological application of the isoperimetric inequality, American Journal of Mathematics 105 (1983), 843–854, Section 1.2, Remark 2, and the special-orthogonal example in Section 3.4 give the following concentration specialization.

abbrev OAI.InvariantIsing.SpecialOrthogonal line 21
def OAI.InvariantIsing.frobeniusDistance line 24
Source documentation
Frobenius distance, with the unnormalized matrix-coordinate convention.
```
def frobeniusDistance {N : ℕ} (U V : SpecialOrthogonal N) : ℝ :=
…
```
Mentions: OAI.InvariantIsing.SpecialOrthogonal
def OAI.InvariantIsing.HaarConcentrationInput line 31
Source documentation
Haar concentration for arbitrary Frobenius-Lipschitz observables on SO(N). The constants are uniform in dimension, observable, and Lipschitz constant.
```
def HaarConcentrationInput : Prop :=
…
```
def OAI.InvariantIsing.GaussianLipschitzVarianceInput line 55
Source documentation
The finite-dimensional Gaussian Poincaré inequality specialized to a globally Lipschitz function. The Euclidean norm is essential: a coordinatewise bound for the supremum norm would introduce a dimension factor.
Published source: Bakry–Émery, Diffusions hypercontractives, Séminaire de Probabilités XIX (1985), Proposition 5, equation (20), p.198, with U(x)=x², and Corollary 2, equation (23), p.199, with the Ornstein–Uhlenbeck example on pp.199–200 (the carré-du-champ calculation is on p.186). The usual Lipschitz specialization follows by smooth approximation.
```
def GaussianLipschitzVarianceInput : Prop :=
…
```