The fourier action component of the Connes rigidity formalization.

@[reducible, inline]

abbrev Connes.PaperFourierAction.D : Type

The D construction used in the Connes rigidity formalization.

Equations

• Connes.PaperFourierAction.D = Connes.Construction.PaperKernel.D

@[reducible, inline]

abbrev Connes.PaperFourierAction.CharacterSpace : Type

The CharacterSpace construction used in the Connes rigidity formalization.

Equations

• Connes.PaperFourierAction.CharacterSpace = Connes.PaperDualHaar.PaperCharacterSpace

@[reducible, inline]

noncomputable abbrev Connes.PaperFourierAction.FourierSpace : AddSubgroup (PaperDualHaar.PaperCharacterSpace →ₘ[PaperDualHaar.paperCharacterHaar] ℂ)

The FourierSpace construction used in the Connes rigidity formalization.

Equations

• Connes.PaperFourierAction.FourierSpace = MeasureTheory.Lp ℂ 2 Connes.PaperDualHaar.paperCharacterHaar

@[instance_reducible]

noncomputable def Connes.PaperFourierAction.paperDDecidableEq : DecidableEq D

The paperDDecidableEq construction used in the Connes rigidity formalization.

Equations

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

@[instance_reducible]

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

The paperMultiplicativeDDecidableEq construction used in the Connes rigidity formalization.

Equations

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

noncomputable def Connes.PaperFourierAction.characterMultiplier : C(CharacterSpace, ℂ) →L[ℂ] ↥FourierSpace →L[ℂ] ↥FourierSpace

The characterMultiplier construction used in the Connes rigidity formalization.

Equations

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

theorem Connes.PaperFourierAction.characterMultiplier_coeFn (q : C(CharacterSpace, ℂ)) (f : ↥FourierSpace) : ↑↑((characterMultiplier q) f) =ᵐ[PaperDualHaar.paperCharacterHaar] fun (χ : PaperDualHaar.PaperCharacterSpace) => q χ * ↑↑f χ

The multiplier has the expected pointwise representative. Paper: §3.

theorem Connes.PaperFourierAction.characterMultiplier_character (d e : D) : (characterMultiplier (PaperFourier.complexCharacter d)) (PaperFourier.characterL2 e) = PaperFourier.characterL2 (d + e)

noncomputable def Connes.PaperFourierAction.paperFourierUnitary : ↥(GroupL2 (Multiplicative D)) ≃ₗᵢ[ℂ] ↥FourierSpace

The paperFourierUnitary construction used in the Connes rigidity formalization.

Equations

• Connes.PaperFourierAction.paperFourierUnitary = (Connes.l2Reindex Multiplicative.toAdd).trans Connes.PaperFourier.FourierTransform

theorem Connes.PaperFourierAction.paperFourierUnitary_single (d : D) : paperFourierUnitary (lp.single 2 (Multiplicative.ofAdd d) 1) = PaperFourier.characterL2 d

theorem Connes.PaperFourierAction.fourier_conjugates_regular_of_character_basis {A : Type u_1} [AddCommGroup A] [DecidableEq A] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (U : ↥(GroupL2 (Multiplicative A)) ≃ₗᵢ[ℂ] K) (χ : A → K) (hU : ∀ (b : A), U (lp.single 2 (Multiplicative.ofAdd b) 1) = χ b) (a : A) (T : K →L[ℂ] K) (hT : ∀ (b : A), T (χ b) = χ (a + b)) : U.conjStarAlgEquiv ↑(leftRegularUnitary (Multiplicative.ofAdd a)) = T

theorem Connes.PaperFourierAction.paperFourier_conjugates_regular (d : D) : paperFourierUnitary.conjStarAlgEquiv ↑(leftRegularUnitary (Multiplicative.ofAdd d)) = characterMultiplier (PaperFourier.complexCharacter d)