Documentation

LeanPool.ConnesRigidity.Paper.Section3.DualHaar

The dual haar component of the Connes rigidity formalization.

source
@[instance_reducible]
noncomputable instance Connes.PaperDualHaar.paperKernelTopology :
TopologicalSpace Construction.PaperKernel.D

The discrete topology on the actual abelian kernel. Paper: §3.

Equations
source
instance Connes.PaperDualHaar.paperKernelDiscreteTopology :
DiscreteTopology Construction.PaperKernel.D

The actual abelian kernel is discrete for the dual construction. Paper: §3.

source
@[reducible, inline]
abbrev Connes.PaperDualHaar.PaperCharacterSpace :
Type

The compact binary character space of the actual kernel. Paper: §3.

Equations
Instances For
    source
    instance Connes.PaperDualHaar.paperKernelMulCountable :
    Countable (Multiplicative Construction.PaperKernel.D)

    The multiplicative copy of Zhou's countable kernel remains countable. Paper: §3.

    source
    instance Connes.PaperDualHaar.paperCharacterSecondCountable :
    SecondCountableTopology PaperCharacterSpace

    The compact dual of Zhou's countable discrete kernel is second countable. Paper: §3.

    source
    @[instance_reducible]
    noncomputable instance Connes.PaperDualHaar.paperCharacterMeasurableSpace :
    MeasurableSpace PaperCharacterSpace

    The Borel measurable structure on the compact character space. Paper: §3.

    Equations
    source
    instance Connes.PaperDualHaar.paperCharacterBorelSpace :
    BorelSpace PaperCharacterSpace

    The character space carries its Borel measurable structure. Paper: §3.

    source
    noncomputable def Connes.PaperDualHaar.paperCharacterHaar :
    MeasureTheory.Measure PaperCharacterSpace

    The normalized Haar probability on the actual character space. Paper: §3.

    Equations
    Instances For
      source
      instance Connes.PaperDualHaar.paperCharacterHaar_isProbability :
      MeasureTheory.IsProbabilityMeasure paperCharacterHaar

      The normalized dual Haar measure is a probability measure. Paper: §3.

      source
      instance Connes.PaperDualHaar.paperCharacterHaar_isAddHaar :
      paperCharacterHaar.IsAddLeftInvariant

      The normalized dual Haar measure is translation invariant. Paper: §3.

      source
      noncomputable def Connes.PaperDualHaar.linearCharacter (ℓ : Construction.PaperKernel.D →ₗ[ZMod 2] ZMod 2) :
      PontryaginDual (Multiplicative Construction.PaperKernel.D)

      A binary linear form gives its continuous circle character. Paper: §3.

      Equations
      Instances For
        source
        @[simp]
        theorem Connes.PaperDualHaar.linearCharacter_apply (ℓ : Construction.PaperKernel.D →ₗ[ZMod 2] ZMod 2) (x : Construction.PaperKernel.D) :
        (linearCharacter ℓ) (Multiplicative.ofAdd x) = ZMod.toCircle (ℓ x)
        source
        theorem Connes.PaperDualHaar.characterLinear_linearCharacter (ℓ : Construction.PaperKernel.D →ₗ[ZMod 2] ZMod 2) :
        BinaryPontryaginDual.characterLinear (linearCharacter ℓ) = ℓ

        Character extraction recovers every binary linear form. Paper: §3.

        source
        theorem Connes.PaperDualHaar.linearCharacter_characterLinear (χ : PontryaginDual (Multiplicative Construction.PaperKernel.D)) :
        linearCharacter (BinaryPontryaginDual.characterLinear χ) = χ

        Every continuous binary character is recovered from its linear form. Paper: §3.

        source
        noncomputable def Connes.PaperDualHaar.characterToLinear :
        PaperCharacterSpace →+ Module.Dual (ZMod 2) Construction.PaperKernel.D

        Character extraction is additive in the binary character group. Paper: §3.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def Connes.PaperDualHaar.linearToCharacter :
          Module.Dual (ZMod 2) Construction.PaperKernel.D →+ PaperCharacterSpace

          A binary linear form is sent to its circle character. Paper: §3.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            noncomputable def Connes.PaperDualHaar.characterLinearEquiv :
            PaperCharacterSpace ≃+ Module.Dual (ZMod 2) Construction.PaperKernel.D

            The actual compact dual is algebraically the full binary linear dual. Paper: §3.

            Equations
            Instances For
              source
              noncomputable def Connes.PaperDualHaar.characterCoordinatesEquiv :
              PaperCharacterSpace ≃+ PaperFactorIsomorphism.DualCoordinates

              The actual Zhou dual coordinates. Paper: §3.

              Equations
              Instances For