Documentation

LeanPool.ConnesRigidity.Paper.Section3.GroupVacuum

The group vacuum component of the Connes rigidity formalization.

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

The D construction used in the Connes rigidity formalization.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev Connes.PaperGroupVacuum.H :
    Type

    The H construction used in the Connes rigidity formalization.

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

      The paperDDecidableEq construction used in the Connes rigidity formalization.

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

        The paperMultiplicativeDDecidableEq construction used in the Connes rigidity formalization.

        Equations
        Instances For
          source
          @[instance_reducible]
          noncomputable def Connes.PaperGroupVacuum.paperGroupOneDecidableEq :
          DecidableEq (Construction.PaperKernel.paperGammaCarrier Construction.PaperKernel.paperThetaOneHom)

          The paperGroupOneDecidableEq construction used in the Connes rigidity formalization.

          Equations
          Instances For
            source
            @[instance_reducible]
            noncomputable def Connes.PaperGroupVacuum.paperGroupTwoDecidableEq :
            DecidableEq (Construction.PaperKernel.paperGammaCarrier Construction.PaperKernel.paperThetaTwoHom)

            The paperGroupTwoDecidableEq construction used in the Connes rigidity formalization.

            Equations
            Instances For
              source
              theorem Connes.PaperGroupVacuum.paperHaarActionOneFinite :
              MeasureTheory.IsFiniteMeasure PaperCrossedHaar.paperHaarActionOne.measure
              source
              theorem Connes.PaperGroupVacuum.paperHaarActionTwoFinite :
              MeasureTheory.IsFiniteMeasure PaperCrossedHaar.paperHaarActionTwo.measure
              source
              noncomputable def Connes.PaperGroupVacuum.paperIdentityOne :
              ↥(GroupL2 (Construction.PaperKernel.paperGammaCarrier Construction.PaperKernel.paperThetaOneHom))

              The paperIdentityOne construction used in the Connes rigidity formalization.

              Equations
              Instances For
                source
                noncomputable def Connes.PaperGroupVacuum.paperIdentityTwo :
                ↥(GroupL2 (Construction.PaperKernel.paperGammaCarrier Construction.PaperKernel.paperThetaTwoHom))

                The paperIdentityTwo construction used in the Connes rigidity formalization.

                Equations
                Instances For
                  source
                  theorem Connes.PaperGroupVacuum.coordinateCharacterL2_zero :
                  PaperFourierCoordinates.coordinateCharacterL2 0 = (MeasureTheory.Lp.const 2 PaperDualTopology.coordinatesHaar) 1
                  source
                  theorem Connes.PaperGroupVacuum.paperGroupFactorUnitaryOne_vacuum :
                  PaperGroupFactor.paperGroupFactorUnitaryOne paperIdentityOne = CrossedProduct.crossedVacuum PaperCrossedHaar.paperHaarActionOne
                  source
                  theorem Connes.PaperGroupVacuum.paperGroupFactorUnitaryTwo_vacuum :
                  PaperGroupFactor.paperGroupFactorUnitaryTwo paperIdentityTwo = CrossedProduct.crossedVacuum PaperCrossedHaar.paperHaarActionTwo