Documentation

LeanPool.ConnesRigidity.Paper.Section4.SpectralFiniteDetection

Finite detector sets for the raw Zhou split extensions. Paper: §4.

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

The k construction used in the Connes rigidity formalization.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev Connes.PaperSpectralFiniteDetection.A :
    Type

    The A construction used in the Connes rigidity formalization.

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

      The D construction used in the Connes rigidity formalization.

      Equations
      Instances For
        source
        @[reducible, inline]
        abbrev Connes.PaperSpectralFiniteDetection.VStar :
        Type

        The VStar construction used in the Connes rigidity formalization.

        Equations
        Instances For
          source
          @[reducible, inline]
          abbrev Connes.PaperSpectralFiniteDetection.SymplecticIndex :
          Type

          The SymplecticIndex construction used in the Connes rigidity formalization.

          Equations
          Instances For
            source
            noncomputable def Connes.PaperSpectralFiniteDetection.aZeroCoeff :
            A →ₗ[k] k

            The aZeroCoeff 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.PaperSpectralFiniteDetection.aZeroCoeff_basisVector_zero :
              aZeroCoeff (PaperFiniteCharts.basisVector 0) = 1

              The coefficient functional takes the base chart vector to one. Paper: §4.

              source
              theorem Connes.PaperSpectralFiniteDetection.aCoordinateEmbedding_injective :
              Function.Injective fun (v : SymplecticIndex) => (PaperAChartDetectorMeasure.aCoordinateEmbedding v) (PaperFiniteCharts.basisVector 0)
              source
              noncomputable def Connes.PaperSpectralFiniteDetection.aDetectorEmbedding :
              SymplecticIndex ↪ D

              The aDetectorEmbedding 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.PaperSpectralFiniteDetection.cDetector :
                D

                The C-coordinate detector singled out by the paper's five-detector bound. Paper: §4.

                Equations
                Instances For
                  source
                  noncomputable def Connes.PaperSpectralFiniteDetection.aDetectorImage :
                  Finset D

                  The finite A-detector image used by the five-detector set. Paper: §4.

                  Equations
                  Instances For
                    source
                    noncomputable def Connes.PaperSpectralFiniteDetection.detectorFinset :
                    Finset D

                    The explicit finite detector set for both raw split extensions. Paper: §4.

                    Equations
                    Instances For
                      source
                      theorem Connes.PaperSpectralFiniteDetection.basisVector_zero_ne_zero :
                      PaperFiniteCharts.basisVector 0 ≠ 0

                      The standard A chart vector is nonzero. Paper: §4.

                      source
                      theorem Connes.PaperSpectralFiniteDetection.diagonal_basisVector_zero_ne_zero :
                      Construction.PaperKernel.diagonal (PaperFiniteCharts.basisVector 0) ≠ 0
                      source
                      theorem Connes.PaperSpectralFiniteDetection.cDetector_not_mem_image :
                      cDetector ∉ aDetectorImage
                      source
                      theorem Connes.PaperSpectralFiniteDetection.detectorFinset_sum_eq (f : D → ℝ) :
                      ∑ d ∈ detectorFinset, f d = ∑ v : SymplecticIndex, f ((PaperAChartDetectorMeasure.aCoordinateEmbedding v) (PaperFiniteCharts.basisVector 0)) + f cDetector
                      source
                      theorem Connes.PaperSpectralFiniteDetection.spectralDetectionEnergy_nonneg (μ : MeasureTheory.ProbabilityMeasure (DiscreteCharacterSpace Construction.PaperKernel.D)) (d : D) :
                      0 ≤ spectralDetectionEnergy μ d
                      source
                      theorem Connes.PaperSpectralFiniteDetection.lambda_one_hasFiniteSpectralDetection :
                      HasFiniteSpectralDetection PaperSpectralPropertyT.lambdaOneExtension detectorFinset (1 / 3)
                      source
                      theorem Connes.PaperSpectralFiniteDetection.lambda_two_hasFiniteSpectralDetection :
                      HasFiniteSpectralDetection PaperSpectralPropertyT.lambdaTwoExtension detectorFinset (1 / 3)
                      source
                      noncomputable def Connes.PaperSpectralFiniteDetection.lambdaOneSpectralData :
                      PaperSpectralPropertyT.SpectralData Construction.PaperKernel.paperThetaOneHom

                      The lambdaOneSpectralData 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.PaperSpectralFiniteDetection.lambdaTwoSpectralData :
                        PaperSpectralPropertyT.SpectralData Construction.PaperKernel.paperThetaTwoHom

                        Package the proved detector set for the second split extension. Paper: §4.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For