Documentation

LeanPool.ConnesRigidity.Paper.Section3.FourierCoordinates

The fourier coordinates component of the Connes rigidity formalization.

source
@[reducible, inline]
abbrev Connes.PaperFourierCoordinates.D :
Type

The D construction used in the Connes rigidity formalization.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev Connes.PaperFourierCoordinates.CharacterSpace :
    Type

    The CharacterSpace construction used in the Connes rigidity formalization.

    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev Connes.PaperFourierCoordinates.Coordinates :
      Type

      The Coordinates construction used in the Connes rigidity formalization.

      Equations
      Instances For
        source
        @[reducible, inline]
        noncomputable abbrev Connes.PaperFourierCoordinates.CharacterL2 :
        AddSubgroup (PaperDualHaar.PaperCharacterSpace →ₘ[PaperDualHaar.paperCharacterHaar] ℂ)

        The CharacterL2 construction used in the Connes rigidity formalization.

        Equations
        Instances For
          source
          @[reducible, inline]
          noncomputable abbrev Connes.PaperFourierCoordinates.CoordinateL2 :
          AddSubgroup (PaperDualTopology.Coordinates →ₘ[PaperDualTopology.coordinatesHaar] ℂ)

          The CoordinateL2 construction used in the Connes rigidity formalization.

          Equations
          Instances For
            source
            @[instance_reducible]
            noncomputable def Connes.PaperFourierCoordinates.paperDDecidableEq :
            DecidableEq D

            The paperDDecidableEq construction used in the Connes rigidity formalization.

            Equations
            Instances For
              source
              @[instance_reducible]
              noncomputable def Connes.PaperFourierCoordinates.paperMultiplicativeDDecidableEq :
              DecidableEq (Multiplicative D)

              The paperMultiplicativeDDecidableEq construction used in the Connes rigidity formalization.

              Equations
              Instances For
                source
                noncomputable def Connes.PaperFourierCoordinates.characterCoordinatesMeasurableEquiv :
                CharacterSpace ≃ᵐ Coordinates

                The characterCoordinatesMeasurableEquiv construction used in the Connes rigidity formalization.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  theorem Connes.PaperFourierCoordinates.characterCoordinates_measurePreserving :
                  MeasureTheory.MeasurePreserving (⇑characterCoordinatesMeasurableEquiv) PaperDualHaar.paperCharacterHaar PaperDualTopology.coordinatesHaar

                  Transport of normalized Haar from the compact dual to Zhou coordinates. Paper: §3.

                  source
                  noncomputable def Connes.PaperFourierCoordinates.characterCoordinatesLpEquiv :
                  ↥CharacterL2 ≃ₗᵢ[ℂ] ↥CoordinateL2

                  The characterCoordinatesLpEquiv construction used in the Connes rigidity formalization.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    @[simp]
                    theorem Connes.PaperFourierCoordinates.characterCoordinatesLpEquiv_apply (f : ↥CharacterL2) :
                    characterCoordinatesLpEquiv f = (MeasureTheory.Lp.compMeasurePreserving ⇑characterCoordinatesMeasurableEquiv.symm ⋯) f
                    source
                    noncomputable def Connes.PaperFourierCoordinates.paperFourierCoordinateUnitary :
                    ↥(GroupL2 (Multiplicative D)) ≃ₗᵢ[ℂ] ↥CoordinateL2

                    The paper Fourier transform with target in Zhou coordinates. Paper: §3.

                    Equations
                    Instances For
                      source
                      noncomputable def Connes.PaperFourierCoordinates.coordinateCharacterL2 (d : D) :
                      ↥CoordinateL2

                      The coordinateCharacterL2 construction used in the Connes rigidity formalization.

                      Equations
                      Instances For
                        source
                        @[simp]
                        theorem Connes.PaperFourierCoordinates.paperFourierCoordinateUnitary_single (d : D) :
                        paperFourierCoordinateUnitary (lp.single 2 (Multiplicative.ofAdd d) 1) = coordinateCharacterL2 d
                        source
                        noncomputable def Connes.PaperFourierCoordinates.coordinateCharacterMultiplier (d : D) :
                        ↥CoordinateL2 →L[ℂ] ↥CoordinateL2

                        The transported kernel multiplier in raw coordinates. Paper: §3.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          theorem Connes.PaperFourierCoordinates.paperFourierCoordinate_conjugates_regular (d : D) :
                          paperFourierCoordinateUnitary.conjStarAlgEquiv ↑(leftRegularUnitary (Multiplicative.ofAdd d)) = coordinateCharacterMultiplier d