Documentation

LeanPool.ConnesRigidity.Paper.Section3.Fourier

The fourier component of the Connes rigidity formalization.

source
@[reducible, inline]
abbrev Connes.PaperFourier.k :
Type

The k construction used in the Connes rigidity formalization.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev Connes.PaperFourier.D :
    Type

    The D construction used in the Connes rigidity formalization.

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

      The CharacterSpace construction used in the Connes rigidity formalization.

      Equations
      Instances For
        source
        noncomputable def Connes.PaperFourier.complexCharacter (d : D) :
        C(CharacterSpace, ℂ)

        The complexCharacter construction used in the Connes rigidity formalization.

        Equations
        Instances For
          source
          @[simp]
          theorem Connes.PaperFourier.complexCharacter_apply (d : D) (χ : CharacterSpace) :
          (complexCharacter d) χ = ↑((Additive.toMul χ) (Multiplicative.ofAdd d))
          source
          theorem Connes.PaperFourier.complexCharacter_separates {χ ψ : CharacterSpace} (hχψ : χ ≠ ψ) :
          ∃ (d : D), (complexCharacter d) χ ≠ (complexCharacter d) ψ

          Characters separate points of the compact dual. Paper: §3.

          source
          noncomputable def Connes.PaperFourier.evaluationCharacter (d : D) :
          PontryaginDual (Multiplicative CharacterSpace)

          The evaluationCharacter 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.PaperFourier.evaluationCharacter_apply (d : D) (χ : CharacterSpace) :
            (evaluationCharacter d) (Multiplicative.ofAdd χ) = (Additive.toMul χ) (Multiplicative.ofAdd d)
            source
            theorem Connes.PaperFourier.evaluationCharacter_ne_one {d : D} (hd : d ≠ 0) :
            evaluationCharacter d ≠ 1
            source
            theorem Connes.PaperFourier.integral_character_eq_zero {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] (μ : MeasureTheory.Measure G) [μ.IsAddLeftInvariant] (χ : PontryaginDual (Multiplicative G)) (hχ : χ ≠ 1) :
            ∫ (x : G), ↑(χ (Multiplicative.ofAdd x)) ∂μ = 0

            A nontrivial continuous character integrates to zero against Haar. Paper: §3.

            source
            noncomputable def Connes.PaperFourier.characterL2 (d : D) :
            ↥(MeasureTheory.Lp ℂ 2 PaperDualHaar.paperCharacterHaar)

            The characterL2 construction used in the Connes rigidity formalization.

            Equations
            Instances For
              source
              theorem Connes.PaperFourier.characterL2_orthonormal :
              Orthonormal ℂ characterL2
              source
              theorem Connes.PaperFourier.complexCharacter_star (d : D) :
              star (complexCharacter d) = complexCharacter (-d)
              source
              noncomputable def Connes.PaperFourier.characterSubalgebra :
              StarSubalgebra ℂ C(CharacterSpace, ℂ)

              The characterSubalgebra construction used in the Connes rigidity formalization.

              Equations
              Instances For
                source
                theorem Connes.PaperFourier.characterSubalgebra_toSubmodule :
                Subalgebra.toSubmodule characterSubalgebra.toSubalgebra = Submodule.span ℂ (Set.range complexCharacter)
                source
                theorem Connes.PaperFourier.complexCharacter_span_closure_eq_top :
                (Submodule.span ℂ (Set.range complexCharacter)).topologicalClosure = ⊤
                source
                theorem Connes.PaperFourier.characterL2_span_closure_eq_top :
                (Submodule.span ℂ (Set.range characterL2)).topologicalClosure = ⊤
                source
                noncomputable def Connes.PaperFourier.FourierBasis :
                HilbertBasis D ℂ ↥(MeasureTheory.Lp ℂ 2 PaperDualHaar.paperCharacterHaar)

                The FourierBasis construction used in the Connes rigidity formalization.

                Equations
                Instances For
                  source
                  @[simp]
                  theorem Connes.PaperFourier.FourierBasis_coe :
                  ⇑FourierBasis = characterL2
                  source
                  noncomputable def Connes.PaperFourier.FourierTransform :
                  ↥(lp (fun (x : D) => ℂ) 2) ≃ₗᵢ[ℂ] ↥(MeasureTheory.Lp ℂ 2 PaperDualHaar.paperCharacterHaar)

                  The FourierTransform construction used in the Connes rigidity formalization.

                  Equations
                  Instances For