The crossed product component of the Connes rigidity formalization.

structure Connes.CrossedProduct.HaarProbabilityAction (K : Type u) (Ω : Type v) [Group K] [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] : Type (max u v)

A probability Haar action is the base input for a crossed-product model. Paper: §3.

• measure : MeasureTheory.Measure Ω

  The measure component of HaarProbabilityAction.

• haar : self.measure.IsAddHaarMeasure
• probability : MeasureTheory.IsProbabilityMeasure self.measure
• action : K →* Equiv.Perm Ω

  The action component of HaarProbabilityAction.

• action_add (k : K) (z z' : Ω) : (self.action k) (z + z') = (self.action k) z + (self.action k) z'
• action_preserves_measure (k : K) : MeasureTheory.MeasurePreserving (⇑(self.action k)) self.measure self.measure

structure Connes.CrossedProduct.EquivariantHaarEquiv {K : Type u} {Ω : Type v} {Ξ : Type w} [Group K] [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] [AddCommGroup Ξ] [TopologicalSpace Ξ] [MeasurableSpace Ξ] (X : HaarProbabilityAction K Ω) (Y : HaarProbabilityAction K Ξ) : Type (max v w)

An equivariant Haar equivalence transports a crossed-product base. Paper: §3.

• toMeasurableEquiv : Ω ≃ᵐ Ξ

  The toMeasurableEquiv component of EquivariantHaarEquiv.

• measure_preserving : MeasureTheory.MeasurePreserving (⇑self.toMeasurableEquiv) X.measure Y.measure
• equivariant (k : K) (z : Ω) : self.toMeasurableEquiv ((X.action k) z) = (Y.action k) (self.toMeasurableEquiv z)

def Connes.CrossedProduct.EquivariantHaarEquiv.refl {K : Type u} {Ω : Type v} [Group K] [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] (X : HaarProbabilityAction K Ω) : EquivariantHaarEquiv X X

The refl construction used in the Connes rigidity formalization.

Equations

• Connes.CrossedProduct.EquivariantHaarEquiv.refl X = { toMeasurableEquiv := MeasurableEquiv.refl Ω, measure_preserving := ⋯, equivariant := ⋯ }

def Connes.CrossedProduct.EquivariantHaarEquiv.symm {K : Type u} {Ω : Type v} {Ξ : Type w} [Group K] [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] [AddCommGroup Ξ] [TopologicalSpace Ξ] [MeasurableSpace Ξ] {X : HaarProbabilityAction K Ω} {Y : HaarProbabilityAction K Ξ} (e : EquivariantHaarEquiv X Y) : EquivariantHaarEquiv Y X

Equivariant Haar equivalences are closed under inverse. Paper: §3.

Equations

• e.symm = { toMeasurableEquiv := e.toMeasurableEquiv.symm, measure_preserving := ⋯, equivariant := ⋯ }

def Connes.CrossedProduct.EquivariantHaarEquiv.trans {K : Type u} {Ω : Type v} {Ξ : Type w} {Ζ : Type x} [Group K] [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] [AddCommGroup Ξ] [TopologicalSpace Ξ] [MeasurableSpace Ξ] [AddCommGroup Ζ] [TopologicalSpace Ζ] [MeasurableSpace Ζ] {X : HaarProbabilityAction K Ω} {Y : HaarProbabilityAction K Ξ} {Z : HaarProbabilityAction K Ζ} (e : EquivariantHaarEquiv X Y) (f : EquivariantHaarEquiv Y Z) : EquivariantHaarEquiv X Z

Equivariant Haar equivalences are closed under composition. Paper: §3.

Equations

• e.trans f = { toMeasurableEquiv := e.toMeasurableEquiv.trans f.toMeasurableEquiv, measure_preserving := ⋯, equivariant := ⋯ }

@[reducible, inline]

noncomputable abbrev Connes.CrossedProduct.crossedBaseHilbert {K : Type u} {Ω : Type v} [Group K] [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] (X : HaarProbabilityAction K Ω) : AddSubgroup (Ω →ₘ[X.measure] ℂ)

The base and crossed-product Hilbert carriers. Paper: §3.

Equations

• Connes.CrossedProduct.crossedBaseHilbert X = MeasureTheory.Lp ℂ 2 X.measure

@[reducible, inline]

noncomputable abbrev Connes.CrossedProduct.crossedHilbert {K : Type u} {Ω : Type v} [Group K] [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] (X : HaarProbabilityAction K Ω) : AddSubgroup (PreLp fun (x : K) => ↥(crossedBaseHilbert X))

The crossedHilbert construction used in the Connes rigidity formalization.

Equations

• Connes.CrossedProduct.crossedHilbert X = lp (fun (x : K) => ↥(Connes.CrossedProduct.crossedBaseHilbert X)) 2

@[reducible, inline]

noncomputable abbrev Connes.CrossedProduct.crossedCoefficient {K : Type u} {Ω : Type v} [Group K] [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] (X : HaarProbabilityAction K Ω) : AddSubgroup (Ω →ₘ[X.measure] ℂ)

The crossedCoefficient construction used in the Connes rigidity formalization.

Equations

• Connes.CrossedProduct.crossedCoefficient X = MeasureTheory.Lp ℂ ⊤ X.measure

noncomputable def Connes.CrossedProduct.crossedBaseMultiplier {K : Type u} {Ω : Type v} [Group K] [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] (X : HaarProbabilityAction K Ω) (f : ↥(crossedCoefficient X)) : ↥(crossedBaseHilbert X) →L[ℂ] ↥(crossedBaseHilbert X)

Multiplication on the base Hilbert space supplies crossed multipliers. Paper: §3.

Equations

• Connes.CrossedProduct.crossedBaseMultiplier X f = (ContinuousLinearMap.holderL X.measure ⊤ 2 2 (ContinuousLinearMap.mul ℂ ℂ)) f

theorem Connes.CrossedProduct.crossedBaseMultiplier_apply_ae {K : Type u} {Ω : Type v} [Group K] [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] (X : HaarProbabilityAction K Ω) (f : ↥(crossedCoefficient X)) (ξ : ↥(crossedBaseHilbert X)) : ↑↑((crossedBaseMultiplier X f) ξ) =ᵐ[X.measure] fun (z : Ω) => ↑↑f z * ↑↑ξ z

The multiplier has its pointwise representative almost everywhere. Paper: §3.

noncomputable def Connes.CrossedProduct.crossedFiberwiseOperator {K : Type u} {H : Type v} [NormedAddCommGroup H] [NormedSpace ℂ H] (T : H →L[ℂ] H) : ↥(lp (fun (x : K) => H) 2) →L[ℂ] ↥(lp (fun (x : K) => H) 2)

The crossedFiberwiseOperator construction used in the Connes rigidity formalization.

Equations

• Connes.CrossedProduct.crossedFiberwiseOperator T = { toFun := fun (ξ : ↥(lp (fun (x : K) => H) 2)) => ⟨fun (k : K) => T (↑ξ k), ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous ‖T‖ ⋯

@[simp]

theorem Connes.CrossedProduct.crossedFiberwiseOperator_apply {K : Type u} {H : Type v} [NormedAddCommGroup H] [NormedSpace ℂ H] (T : H →L[ℂ] H) (ξ : ↥(lp (fun (x : K) => H) 2)) (k : K) : ↑((crossedFiberwiseOperator T) ξ) k = T (↑ξ k)

noncomputable def Connes.CrossedProduct.crossedMultiplier {K : Type u} {Ω : Type v} [Group K] [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] (X : HaarProbabilityAction K Ω) (f : ↥(crossedCoefficient X)) : ↥(crossedHilbert X) →L[ℂ] ↥(crossedHilbert X)

Base multipliers are lifted fiberwise to the crossed Hilbert space. Paper: §3.

Equations

• Connes.CrossedProduct.crossedMultiplier X f = Connes.CrossedProduct.crossedFiberwiseOperator (Connes.CrossedProduct.crossedBaseMultiplier X f)

@[simp]

theorem Connes.CrossedProduct.crossedMultiplier_apply {K : Type u} {Ω : Type v} [Group K] [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] (X : HaarProbabilityAction K Ω) (f : ↥(crossedCoefficient X)) (ξ : ↥(crossedHilbert X)) (k : K) : ↑((crossedMultiplier X f) ξ) k = (crossedBaseMultiplier X f) (↑ξ k)

def Connes.CrossedProduct.crossedFiberwiseEquiv {K : Type u} {H : Type v} {J : Type w} [NormedAddCommGroup H] [NormedSpace ℂ H] [NormedAddCommGroup J] [NormedSpace ℂ J] (e : H ≃ₗᵢ[ℂ] J) : ↥(lp (fun (x : K) => H) 2) ≃ₗᵢ[ℂ] ↥(lp (fun (x : K) => J) 2)

A fiberwise linear isometry is lifted to the crossed Hilbert space. Paper: §3.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Connes.CrossedProduct.crossedFiberwiseEquiv_apply {K : Type u} {H : Type v} {J : Type w} [NormedAddCommGroup H] [NormedSpace ℂ H] [NormedAddCommGroup J] [NormedSpace ℂ J] (e : H ≃ₗᵢ[ℂ] J) (ξ : ↥(lp (fun (x : K) => H) 2)) (k : K) : ↑((crossedFiberwiseEquiv e) ξ) k = e (↑ξ k)

def Connes.CrossedProduct.crossedIndexEquiv {K : Type u} {H : Type v} [NormedAddCommGroup H] [NormedSpace ℂ H] (e : K ≃ K) : ↥(lp (fun (x : K) => H) 2) ≃ₗᵢ[ℂ] ↥(lp (fun (x : K) => H) 2)

The crossed Hilbert space reindexes under a group equivalence. Paper: §3.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Connes.CrossedProduct.crossedIndexEquiv_apply {K : Type u} {H : Type v} [NormedAddCommGroup H] [NormedSpace ℂ H] (e : K ≃ K) (ξ : ↥(lp (fun (x : K) => H) 2)) (k : K) : ↑((crossedIndexEquiv e) ξ) k = ↑ξ (e.symm k)

noncomputable def Connes.CrossedProduct.crossedBaseHaarEquiv {K : Type u} {Ω : Type v} {Ξ : Type w} [Group K] [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] [AddCommGroup Ξ] [TopologicalSpace Ξ] [MeasurableSpace Ξ] {X : HaarProbabilityAction K Ω} {Y : HaarProbabilityAction K Ξ} (e : EquivariantHaarEquiv X Y) : ↥(crossedBaseHilbert X) ≃ₗᵢ[ℂ] ↥(crossedBaseHilbert Y)

The base Haar equivalence acts fiberwise on the crossed Hilbert space. Paper: §3.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Connes.CrossedProduct.crossedBaseHaarEquiv_apply {K : Type u} {Ω : Type v} {Ξ : Type w} [Group K] [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] [AddCommGroup Ξ] [TopologicalSpace Ξ] [MeasurableSpace Ξ] {X : HaarProbabilityAction K Ω} {Y : HaarProbabilityAction K Ξ} (e : EquivariantHaarEquiv X Y) (f : ↥(crossedBaseHilbert X)) : (crossedBaseHaarEquiv e) f = (MeasureTheory.Lp.compMeasurePreserving ⇑e.toMeasurableEquiv.symm ⋯) f

noncomputable def Connes.CrossedProduct.crossedActionL2Equiv {K : Type u} {Ω : Type v} [Group K] [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] (X : HaarProbabilityAction K Ω) (k : K) : ↥(crossedBaseHilbert X) ≃ₗᵢ[ℂ] ↥(crossedBaseHilbert X)

The crossed-product group unitary implements the action on the base. Paper: §3.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Connes.CrossedProduct.crossedActionL2Equiv_apply {K : Type u} {Ω : Type v} [Group K] [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] (X : HaarProbabilityAction K Ω) (k : K) (f : ↥(crossedBaseHilbert X)) : (crossedActionL2Equiv X k) f = (MeasureTheory.Lp.compMeasurePreserving ⇑(X.action k⁻¹) ⋯) f

noncomputable def Connes.CrossedProduct.crossedGroupUnitary {K : Type u} {Ω : Type v} [Group K] [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] (X : HaarProbabilityAction K Ω) (k : K) : ↥(crossedHilbert X) ≃ₗᵢ[ℂ] ↥(crossedHilbert X)

The crossed-product group unitary on the indexed Hilbert space. Paper: §3.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Connes.CrossedProduct.crossedGroupUnitary_apply {K : Type u} {Ω : Type v} [Group K] [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] (X : HaarProbabilityAction K Ω) (k : K) (ξ : ↥(crossedHilbert X)) (h : K) : ↑((crossedGroupUnitary X k) ξ) h = (crossedActionL2Equiv X k) (↑ξ (k⁻¹ * h))

def Connes.CrossedProduct.crossedGeneratorSet {K : Type u} {Ω : Type v} [Group K] [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] (X : HaarProbabilityAction K Ω) : Set (↥(crossedHilbert X) →L[ℂ] ↥(crossedHilbert X))

The standard two-family crossed-product generator set. Paper: §3.

Equations

• Connes.CrossedProduct.crossedGeneratorSet X = Set.range (Connes.CrossedProduct.crossedMultiplier X) ∪ Set.range fun (k : K) => ↑↑(Connes.CrossedProduct.crossedGroupUnitary X k)

noncomputable def Connes.CrossedProduct.crossedVacuum {K : Type u} {Ω : Type v} [Group K] [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] (X : HaarProbabilityAction K Ω) : ↥(crossedHilbert X)

The crossed-product vacuum is the constant base vector at the identity. Paper: §3.

Equations

• Connes.CrossedProduct.crossedVacuum X = lp.single 2 1 ((MeasureTheory.Lp.const 2 X.measure) 1)

structure Connes.CrossedProduct.CrossedProductModel {K : Type u} {Ω : Type v} [Group K] [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] (X : HaarProbabilityAction K Ω) : Type (max u v)

The crossed-product model packages its generated algebra and vacuum state. Paper: §3.

• algebra : VonNeumannAlgebra ↥(crossedHilbert X)

  The algebra component of CrossedProductModel.

• trace : ↥self.algebra.toStarSubalgebra → ℂ

  The trace component of CrossedProductModel.

noncomputable def Connes.CrossedProduct.crossedProductModel {K : Type u} {Ω : Type v} [Group K] [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] (X : HaarProbabilityAction K Ω) : CrossedProductModel X

The crossedProductModel construction used in the Connes rigidity formalization.

Equations

• One or more equations did not get rendered due to their size.