The paper-facing spectral-energy form of Zhou's five-detector estimate. Paper: §4.

@[reducible, inline]

abbrev Connes.PaperSpectralDetector.k : Type

The k construction used in the Connes rigidity formalization.

Equations

• Connes.PaperSpectralDetector.k = Connes.Construction.k

@[reducible, inline]

abbrev Connes.PaperSpectralDetector.D : Type

The D construction used in the Connes rigidity formalization.

Equations

• Connes.PaperSpectralDetector.D = Connes.Construction.PaperKernel.D

@[reducible, inline]

abbrev Connes.PaperSpectralDetector.CharacterSpace : Type

The CharacterSpace construction used in the Connes rigidity formalization.

Equations

• Connes.PaperSpectralDetector.CharacterSpace = Connes.PaperDualHaar.PaperCharacterSpace

noncomputable def Connes.PaperSpectralDetector.detectorValue (χ : CharacterSpace) (d : D) : k

The detectorValue construction used in the Connes rigidity formalization.

Equations

• Connes.PaperSpectralDetector.detectorValue χ d = (Connes.BinaryPontryaginDual.characterLinear (Additive.toMul χ)) d

noncomputable def Connes.PaperSpectralDetector.spectralEnergy (μ : MeasureTheory.ProbabilityMeasure CharacterSpace) (d : D) : ℝ

The squared displacement of a character at one kernel element. Its exact detector-mass value is proved immediately below. Paper: §4.

Equations

• Connes.PaperSpectralDetector.spectralEnergy μ d = ∫ (χ : Connes.PaperSpectralDetector.CharacterSpace), ‖↑(ZMod.toCircle (Connes.PaperSpectralDetector.detectorValue χ d)) - 1‖ ^ 2 ∂↑μ

noncomputable def Connes.PaperSpectralDetector.trivialAtom (μ : MeasureTheory.ProbabilityMeasure CharacterSpace) : ℝ

The mass of the trivial character in the additive dual model. Paper: §4.

Equations

• Connes.PaperSpectralDetector.trivialAtom μ = (↑μ).real {0}

theorem Connes.PaperSpectralDetector.detectorValue_eq_zero_or_one (χ : CharacterSpace) (d : D) : detectorValue χ d = 0 ∨ detectorValue χ d = 1

theorem Connes.PaperSpectralDetector.detectorEnergy_eq_four_indicator (χ : CharacterSpace) (d : D) : ‖↑(ZMod.toCircle (detectorValue χ d)) - 1‖ ^ 2 = 4 * (PaperChartMeasure.linearDetector d).indicator (fun (x : PaperChartMeasure.CharacterSpace) => 1) χ

theorem Connes.PaperSpectralDetector.spectralEnergy_eq_four_mul_measure (μ : MeasureTheory.ProbabilityMeasure CharacterSpace) (d : D) : spectralEnergy μ d = 4 * (↑μ).real (PaperChartMeasure.linearDetector d)

theorem Connes.PaperSpectralDetector.fullNonzeroLocus_eq_zero_compl : PaperFullDetectorMeasure.fullNonzeroLocus = {0}ᶜ

theorem Connes.PaperSpectralDetector.measurableSet_zero : MeasurableSet {0}

theorem Connes.PaperSpectralDetector.fullNonzeroLocus_measureReal_eq_one_sub_trivialAtom (μ : MeasureTheory.ProbabilityMeasure CharacterSpace) : (↑μ).real PaperFullDetectorMeasure.fullNonzeroLocus = 1 - trivialAtom μ

theorem Connes.PaperSpectralDetector.full_spectral_detection (μ : MeasureTheory.ProbabilityMeasure CharacterSpace) (hinv : PaperChartDetectorMeasure.IsInvariantPaperSL3SpectralMeasure μ) : 1 / 3 * (1 - trivialAtom μ) ≤ ∑ v : OpenAIPort.SymplecticIndex, spectralEnergy μ ((PaperAChartDetectorMeasure.aCoordinateEmbedding v) (PaperFiniteCharts.basisVector 0)) + spectralEnergy μ (0, Construction.PaperKernel.diagonal (PaperFiniteCharts.basisVector 0))