Documentation

LeanPool.ConnesRigidity.Paper.Section3.CrossedHaar

The crossed haar component of the Connes rigidity formalization.

source
@[reducible, inline]
abbrev Connes.PaperCrossedHaar.H :
Type

The H construction used in the Connes rigidity formalization.

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

    The Coordinates construction used in the Connes rigidity formalization.

    Equations
    Instances For
      source
      theorem Connes.PaperCrossedHaar.paperCoordinateActionOne_symm (h : H) :
      (PaperDualActions.paperCoordinateActionOne h).symm = PaperDualActions.paperCoordinateActionOne h⁻¹
      source
      theorem Connes.PaperCrossedHaar.paperCoordinateActionTwo_symm (h : H) :
      (PaperDualActions.paperCoordinateActionTwo h).symm = PaperDualActions.paperCoordinateActionTwo h⁻¹
      source
      theorem Connes.PaperCrossedHaar.paperCoordinateActionOne_measurePreserving (h : H) :
      MeasureTheory.MeasurePreserving (⇑(PaperDualActions.paperCoordinateActionOne h)) PaperDualTopology.coordinatesHaar PaperDualTopology.coordinatesHaar
      source
      theorem Connes.PaperCrossedHaar.paperCoordinateActionTwo_measurePreserving (h : H) :
      MeasureTheory.MeasurePreserving (⇑(PaperDualActions.paperCoordinateActionTwo h)) PaperDualTopology.coordinatesHaar PaperDualTopology.coordinatesHaar
      source
      noncomputable def Connes.PaperCrossedHaar.paperHaarActionOne :
      CrossedProduct.HaarProbabilityAction H Coordinates

      The paperHaarActionOne construction used in the Connes rigidity formalization.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def Connes.PaperCrossedHaar.paperHaarActionTwo :
        CrossedProduct.HaarProbabilityAction H Coordinates

        The second Zhou action packaged as a probability Haar action. Paper: §3.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def Connes.PaperCrossedHaar.paperFiberShearHomeomorph :
          Coordinates ≃ₜ Coordinates

          The quadratic fiber shear as a homeomorphism. Its inverse is the same quadratic shear, but it need not preserve the compact-group law. Paper: §3.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            noncomputable def Connes.PaperCrossedHaar.paperFiberShearMeasurableEquiv :
            Coordinates ≃ᵐ Coordinates

            The measurable equivalence underlying the quadratic fiber shear. Paper: §3.

            Equations
            Instances For
              source
              noncomputable def Connes.PaperCrossedHaar.paperHaarHomeomorph :
              CrossedProduct.EquivariantHaarHomeomorph paperHaarActionOne paperHaarActionTwo

              Zhou's fiber shear as an equivariant measure-preserving homeomorphism of the two crossed-product bases. Paper: §3.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                noncomputable def Connes.PaperCrossedHaar.paperHaarEquiv :
                CrossedProduct.EquivariantHaarEquiv paperHaarActionOne paperHaarActionTwo

                Zhou's fiber shear is an equivariant Haar equivalence between the two crossed-product bases. Paper: §3.

                Equations
                Instances For