The crossed kernel component of the Connes rigidity formalization.

@[reducible, inline]

abbrev Connes.PaperCrossedKernel.D : Type

The D construction used in the Connes rigidity formalization.

Equations

• Connes.PaperCrossedKernel.D = Connes.Construction.PaperKernel.D

@[reducible, inline]

abbrev Connes.PaperCrossedKernel.H : Type

The H construction used in the Connes rigidity formalization.

Equations

• Connes.PaperCrossedKernel.H = Connes.Construction.H

@[reducible, inline]

abbrev Connes.PaperCrossedKernel.Coordinates : Type

The Coordinates construction used in the Connes rigidity formalization.

Equations

• Connes.PaperCrossedKernel.Coordinates = Connes.PaperFactorIsomorphism.DualCoordinates

@[reducible, inline]

noncomputable abbrev Connes.PaperCrossedKernel.CoordinateL2 : AddSubgroup (PaperDualTopology.Coordinates →ₘ[PaperDualTopology.coordinatesHaar] ℂ)

The CoordinateL2 construction used in the Connes rigidity formalization.

Equations

• Connes.PaperCrossedKernel.CoordinateL2 = MeasureTheory.Lp ℂ 2 Connes.PaperDualTopology.coordinatesHaar

@[reducible, inline]

noncomputable abbrev Connes.PaperCrossedKernel.X : CrossedProduct.HaarProbabilityAction PaperCrossedHaar.H PaperCrossedHaar.Coordinates

The X construction used in the Connes rigidity formalization.

Equations

• Connes.PaperCrossedKernel.X = Connes.PaperCrossedHaar.paperHaarActionOne

@[reducible, inline]

noncomputable abbrev Connes.PaperCrossedKernel.CrossedL2 : AddSubgroup (PreLp fun (x : PaperCrossedHaar.H) => ↥(CrossedProduct.crossedBaseHilbert X))

The CrossedL2 construction used in the Connes rigidity formalization.

Equations

• Connes.PaperCrossedKernel.CrossedL2 = Connes.CrossedProduct.crossedHilbert Connes.PaperCrossedKernel.X

@[reducible, inline]

noncomputable abbrev Connes.PaperCrossedKernel.FiberL2 : AddSubgroup (PreLp fun (x : Multiplicative D) => ℂ)

The FiberL2 construction used in the Connes rigidity formalization.

Equations

• Connes.PaperCrossedKernel.FiberL2 = Connes.GroupL2 (Multiplicative Connes.PaperCrossedKernel.D)

@[reducible, inline]

noncomputable abbrev Connes.PaperCrossedKernel.ProductL2 : AddSubgroup (PreLp fun (x : H) => ↥FiberL2)

The ProductL2 construction used in the Connes rigidity formalization.

Equations

• Connes.PaperCrossedKernel.ProductL2 = lp (fun (x : Connes.PaperCrossedKernel.H) => ↥Connes.PaperCrossedKernel.FiberL2) 2

@[instance_reducible]

noncomputable def Connes.PaperCrossedKernel.paperDDecidableEq : DecidableEq D

The paperDDecidableEq construction used in the Connes rigidity formalization.

Equations

• Connes.PaperCrossedKernel.paperDDecidableEq = Classical.decEq Connes.PaperCrossedKernel.D

@[instance_reducible]

noncomputable def Connes.PaperCrossedKernel.paperMultiplicativeDDecidableEq : DecidableEq (Multiplicative D)

The paperMultiplicativeDDecidableEq construction used in the Connes rigidity formalization.

Equations

• Connes.PaperCrossedKernel.paperMultiplicativeDDecidableEq = Classical.decEq (Multiplicative Connes.PaperCrossedKernel.D)

noncomputable def Connes.PaperCrossedKernel.coordinateComplexCharacter (d : D) : C(Coordinates, ℂ)

The coordinateComplexCharacter construction used in the Connes rigidity formalization.

Equations

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

@[simp]

theorem Connes.PaperCrossedKernel.coordinateComplexCharacter_apply (d : D) (p : Coordinates) : (coordinateComplexCharacter d) p = (PaperFourier.complexCharacter d) (PaperDualTopology.characterCoordinatesHomeomorph.symm p)

noncomputable def Connes.PaperCrossedKernel.coordinateCharacterCoefficient (d : D) : ↥(CrossedProduct.crossedCoefficient X)

The bounded coefficient used by the crossed base multiplier. Paper: §3.

Equations

• Connes.PaperCrossedKernel.coordinateCharacterCoefficient d = (ContinuousMap.toLp ⊤ Connes.PaperDualTopology.coordinatesHaar ℂ) (Connes.PaperCrossedKernel.coordinateComplexCharacter d)

theorem Connes.PaperCrossedKernel.coordinateCharacterCoefficient_apply_ae (d : D) : ↑↑(coordinateCharacterCoefficient d) =ᵐ[PaperDualTopology.coordinatesHaar] ⇑(coordinateComplexCharacter d)

theorem Connes.PaperCrossedKernel.coordinateCharacterMultiplier_eq_baseMultiplier (d : D) : PaperFourierCoordinates.coordinateCharacterMultiplier d = CrossedProduct.crossedBaseMultiplier X (coordinateCharacterCoefficient d)

The transported multiplier is the concrete crossed-base multiplier. Paper: §3.

noncomputable def Connes.PaperCrossedKernel.paperCrossedKernelFourierUnitary : ↥ProductL2 ≃ₗᵢ[ℂ] ↥CrossedL2

The paperCrossedKernelFourierUnitary construction used in the Connes rigidity formalization.

Equations

• Connes.PaperCrossedKernel.paperCrossedKernelFourierUnitary = Connes.CrossedProduct.crossedFiberwiseEquiv Connes.PaperFourierCoordinates.paperFourierCoordinateUnitary

@[simp]

theorem Connes.PaperCrossedKernel.paperCrossedKernelFourierUnitary_apply (ξ : ↥ProductL2) (h : H) : ↑(paperCrossedKernelFourierUnitary ξ) h = PaperFourierCoordinates.paperFourierCoordinateUnitary (↑ξ h)

noncomputable def Connes.PaperCrossedKernel.productKernelRegularUnitary (d : D) : ↥ProductL2 ≃ₗᵢ[ℂ] ↥ProductL2

The kernel translation on the product fiber model. Paper: §3.

Equations

• Connes.PaperCrossedKernel.productKernelRegularUnitary d = Connes.CrossedProduct.crossedFiberwiseEquiv (Unitary.linearIsometryEquiv (Connes.leftRegularUnitary (Multiplicative.ofAdd d)))

noncomputable def Connes.PaperCrossedKernel.crossedKernelMultiplier (d : D) : ↥CrossedL2 →L[ℂ] ↥CrossedL2

The kernel translation on the concrete crossed base. Paper: §3.

Equations

• Connes.PaperCrossedKernel.crossedKernelMultiplier d = Connes.CrossedProduct.crossedMultiplier Connes.PaperCrossedKernel.X (Connes.PaperCrossedKernel.coordinateCharacterCoefficient d)

theorem Connes.PaperCrossedKernel.paperCrossedKernelFourier_conjugates_regular (d : D) : paperCrossedKernelFourierUnitary.conjStarAlgEquiv ↑↑(productKernelRegularUnitary d) = crossedKernelMultiplier d