NonsingularBoundary.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Nonsingular boundary actions and simultaneous representatives

The action preserves null sets, not necessarily the measure. Countability allows all the identities used in the boundary argument to hold on one invariant conull set. The final definition isolates the exact unitary coefficient property in Björklund, arXiv:1406.0763, Theorem 2.1 and Remark 2.2, expressed as a property of the unitary coefficients.

structure OAI.KadisonKastler.NonsingularAction line 25
Source documentation
A measurable group action preserving the measure class.
```
structure NonsingularAction (G D : Type*) [Group G] [MeasurableSpace D]
    (μ : Measure D) where
…
```
theorem OAI.KadisonKastler.NonsingularAction.one_apply line 35
theorem OAI.KadisonKastler.NonsingularAction.mul_apply line 40
def OAI.KadisonKastler.NonsingularAction.prod line 46
Source documentation
The separate action on the product is again nonsingular.
```
def prod [SFinite μ] : NonsingularAction (G × G) (D × D) (μ.prod μ) where
…
```
Mentions: OAI.KadisonKastler.NonsingularAction
theorem OAI.KadisonKastler.NonsingularAction.prod_apply line 54
def OAI.KadisonKastler.NonsingularAction.diagonal line 58
Source documentation
Restricting the separate action to the diagonal.
```
def diagonal [SFinite μ] : NonsingularAction G (D × D) (μ.prod μ) where
…
```
Mentions: OAI.KadisonKastler.NonsingularAction
theorem OAI.KadisonKastler.NonsingularAction.diagonal_apply line 66

theorem OAI.KadisonKastler.NonsingularAction.exists_invariant_conull line 71

Source documentation

Countably many almost-everywhere properties, together with all their translates, hold on a single invariant conull set.

theorem exists_invariant_conull [Countable G] {ι : Type*} [Countable ι]
    (P : ι → D → Prop) (hP : ∀ i, ∀ᵐ x ∂μ, P i x) :
    ∃ S : Set D, (∀ᵐ x ∂μ, x ∈ S) ∧
      (∀ g x, x ∈ S → α.toPerm g x ∈ S) ∧
      (∀ x ∈ S, ∀ i, P i x) := by
…

theorem OAI.KadisonKastler.NonsingularAction.exists_simultaneous_point line 86

Source documentation

A conull set contains a point when the measure is nonzero.

theorem exists_simultaneous_point [Countable G] [NeZero μ]
    {ι : Type*} [Countable ι] (P : ι → D → Prop)
    (hP : ∀ i, ∀ᵐ x ∂μ, P i x) :
    ∃ x, ∀ g i, P i (α.toPerm g x) := by
…

theorem OAI.KadisonKastler.NonsingularAction.fixed_of_ae_constant line 97
Source documentation
If an equivariant function is almost everywhere constant, its constant value is fixed. This uses nonsingularity and does not use invariance of μ.
```
theorem fixed_of_ae_constant [NeZero μ]
    {E : Type*} (σ : G → E → E) (f : D → E) (v : E)
    (hf : f =ᵐ[μ] fun _ => v)
    (heq : ∀ g, ∀ᵐ x ∂μ, f (α.toPerm g x) = σ g (f x)) :
    ∀ g, σ g v = v := by
…
```
def OAI.KadisonKastler.UnitaryDoubleErgodic line 117
Source documentation
The exact double-ergodicity property with unitary coefficients used below. It is the bounded-map specialization of Björklund's Theorem 2.1, Remark 2.2 (arXiv:1406.0763), for a symmetric Poisson boundary.
```
def UnitaryDoubleErgodic (α : NonsingularAction G D μ) : Prop :=
…
```
Mentions: OAI.KadisonKastler.NonsingularAction