Transport of Zhou's compact-dual detector estimate to the raw Pontryagin-dual carrier used by the generic split-extension criterion. Paper: §4.

@[reducible, inline]

abbrev Connes.PaperSpectralDetectorBridge.Raw : Type

The Raw construction used in the Connes rigidity formalization.

Equations

• Connes.PaperSpectralDetectorBridge.Raw = Connes.DiscreteCharacterSpace Connes.Construction.PaperKernel.D

@[reducible, inline]

abbrev Connes.PaperSpectralDetectorBridge.Paper : Type

The Paper construction used in the Connes rigidity formalization.

Equations

• Connes.PaperSpectralDetectorBridge.Paper = Connes.PaperSpectralDetector.CharacterSpace

def Connes.PaperSpectralDetectorBridge.rawToPaper : Raw ≃ Paper

The rawToPaper construction used in the Connes rigidity formalization.

Equations

• Connes.PaperSpectralDetectorBridge.rawToPaper = Additive.ofMul

theorem Connes.PaperSpectralDetectorBridge.rawToPaper_measurable : Measurable ⇑rawToPaper

The type-tag equivalence is measurable for the transported Borel models. Paper: §3.

theorem Connes.PaperSpectralDetectorBridge.paperToRaw_measurable : Measurable ⇑rawToPaper.symm

noncomputable def Connes.PaperSpectralDetectorBridge.paperMeasureOfRaw (μ : MeasureTheory.ProbabilityMeasure Raw) : MeasureTheory.ProbabilityMeasure Paper

The paperMeasureOfRaw construction used in the Connes rigidity formalization.

Equations

• Connes.PaperSpectralDetectorBridge.paperMeasureOfRaw μ = μ.map ⋯

theorem Connes.PaperSpectralDetectorBridge.raw_action_to_paper {H : CountableDiscreteGroup} (action : H.Carrier →* Multiplicative (AddAut Construction.PaperKernel.D)) (h : H.Carrier) (χ : Raw) : rawToPaper (dualCharacterAction action h χ) = PaperChartMeasure.paperDualCharacterAction action h (rawToPaper χ)

theorem Connes.PaperSpectralDetectorBridge.paper_measure_invariant_of_raw {H : CountableDiscreteGroup} (action : H.Carrier →* Multiplicative (AddAut Construction.PaperKernel.D)) (μ : MeasureTheory.ProbabilityMeasure Raw) (hinv : IsInvariantSpectralMeasure action μ) : PaperChartMeasure.IsInvariantPaperSpectralMeasure action (paperMeasureOfRaw μ)

theorem Connes.PaperSpectralDetectorBridge.energy_transport (μ : MeasureTheory.ProbabilityMeasure Raw) (d : Construction.PaperKernel.D) : PaperSpectralDetector.spectralEnergy (paperMeasureOfRaw μ) d = spectralDetectionEnergy μ d

theorem Connes.PaperSpectralDetectorBridge.trivial_atom_transport (μ : MeasureTheory.ProbabilityMeasure Raw) : PaperSpectralDetector.trivialAtom (paperMeasureOfRaw μ) = spectralTrivialAtom μ

theorem Connes.PaperSpectralDetectorBridge.raw_full_spectral_detection_of_paper_sl3_invariance (μ : MeasureTheory.ProbabilityMeasure Raw) (hinv : PaperChartDetectorMeasure.IsInvariantPaperSL3SpectralMeasure (paperMeasureOfRaw μ)) : 1 / 3 * (1 - spectralTrivialAtom μ) ≤ ∑ v : OpenAIPort.SymplecticIndex, spectralDetectionEnergy μ ((PaperAChartDetectorMeasure.aCoordinateEmbedding v) (PaperFiniteCharts.basisVector 0)) + spectralDetectionEnergy μ (0, Construction.PaperKernel.diagonal (PaperFiniteCharts.basisVector 0))

theorem Connes.PaperSpectralDetectorBridge.raw_full_spectral_detection (μ : MeasureTheory.ProbabilityMeasure Raw) (hinv : IsInvariantSpectralMeasure PaperChartDetectorMeasure.paperThetaOneAddAction μ) : 1 / 3 * (1 - spectralTrivialAtom μ) ≤ ∑ v : OpenAIPort.SymplecticIndex, spectralDetectionEnergy μ ((PaperAChartDetectorMeasure.aCoordinateEmbedding v) (PaperFiniteCharts.basisVector 0)) + spectralDetectionEnergy μ (0, Construction.PaperKernel.diagonal (PaperFiniteCharts.basisVector 0))

theorem Connes.PaperSpectralDetectorBridge.lambda_one_paper_sl3_invariance (μ : MeasureTheory.ProbabilityMeasure Raw) (hinv : IsInvariantSpectralMeasure PaperSpectralPropertyT.lambdaOneExtension.action μ) : PaperChartDetectorMeasure.IsInvariantPaperSL3SpectralMeasure (paperMeasureOfRaw μ)

theorem Connes.PaperSpectralDetectorBridge.paper_theta_two_sl3_addAction_eq (g : SpecialLinear.SL3) : PaperChartDetectorMeasure.paperThetaTwoAddAction (g, 1) = PaperChartDetectorMeasure.paperThetaOneAddAction (g, 1)

theorem Connes.PaperSpectralDetectorBridge.lambda_two_paper_sl3_invariance (μ : MeasureTheory.ProbabilityMeasure Raw) (hinv : IsInvariantSpectralMeasure PaperSpectralPropertyT.lambdaTwoExtension.action μ) : PaperChartDetectorMeasure.IsInvariantPaperSL3SpectralMeasure (paperMeasureOfRaw μ)

theorem Connes.PaperSpectralDetectorBridge.lambda_one_full_spectral_detection (μ : MeasureTheory.ProbabilityMeasure Raw) (hinv : IsInvariantSpectralMeasure PaperSpectralPropertyT.lambdaOneExtension.action μ) : 1 / 3 * (1 - spectralTrivialAtom μ) ≤ ∑ v : OpenAIPort.SymplecticIndex, spectralDetectionEnergy μ ((PaperAChartDetectorMeasure.aCoordinateEmbedding v) (PaperFiniteCharts.basisVector 0)) + spectralDetectionEnergy μ (0, Construction.PaperKernel.diagonal (PaperFiniteCharts.basisVector 0))

theorem Connes.PaperSpectralDetectorBridge.lambda_two_full_spectral_detection (μ : MeasureTheory.ProbabilityMeasure Raw) (hinv : IsInvariantSpectralMeasure PaperSpectralPropertyT.lambdaTwoExtension.action μ) : 1 / 3 * (1 - spectralTrivialAtom μ) ≤ ∑ v : OpenAIPort.SymplecticIndex, spectralDetectionEnergy μ ((PaperAChartDetectorMeasure.aCoordinateEmbedding v) (PaperFiniteCharts.basisVector 0)) + spectralDetectionEnergy μ (0, Construction.PaperKernel.diagonal (PaperFiniteCharts.basisVector 0))