Full §4 detector union for Zhou's compact dual. Paper: §4.

@[reducible, inline]

abbrev Connes.PaperFullDetectorMeasure.k : Type

The k construction used in the Connes rigidity formalization.

Equations

• Connes.PaperFullDetectorMeasure.k = Connes.Construction.k

@[reducible, inline]

abbrev Connes.PaperFullDetectorMeasure.D : Type

The D construction used in the Connes rigidity formalization.

Equations

• Connes.PaperFullDetectorMeasure.D = Connes.Construction.PaperKernel.D

@[reducible, inline]

abbrev Connes.PaperFullDetectorMeasure.A : Type

The A construction used in the Connes rigidity formalization.

Equations

• Connes.PaperFullDetectorMeasure.A = Connes.Construction.A

@[reducible, inline]

abbrev Connes.PaperFullDetectorMeasure.C : Submodule Construction.k Construction.PaperKernel.TensorAA

The C construction used in the Connes rigidity formalization.

Equations

• Connes.PaperFullDetectorMeasure.C = Connes.Construction.PaperKernel.C

@[reducible, inline]

abbrev Connes.PaperFullDetectorMeasure.CharacterSpace : Type

The CharacterSpace construction used in the Connes rigidity formalization.

Equations

• Connes.PaperFullDetectorMeasure.CharacterSpace = Connes.PaperDualTopology.CharacterSpace

@[reducible, inline]

abbrev Connes.PaperFullDetectorMeasure.SymplecticIndex : Type

The SymplecticIndex construction used in the Connes rigidity formalization.

Equations

• Connes.PaperFullDetectorMeasure.SymplecticIndex = Connes.OpenAIPort.SymplecticIndex

theorem Connes.PaperFullDetectorMeasure.aChartLinear_eq_coordinate (χ : CharacterSpace) (v : SymplecticIndex) (a : A) : (PaperAChartDetectorMeasure.aChartLinear χ v) a = (PaperDualHaar.characterCoordinatesEquiv χ).1 a v

The A-coordinate value agrees with Zhou's transported dual coordinates. Paper: §3.

def Connes.PaperFullDetectorMeasure.fullNonzeroLocus : Set CharacterSpace

The fullNonzeroLocus construction used in the Connes rigidity formalization.

Equations

• Connes.PaperFullDetectorMeasure.fullNonzeroLocus = {χ : Connes.PaperFullDetectorMeasure.CharacterSpace | Connes.PaperDualHaar.characterLinearEquiv χ ≠ 0}

theorem Connes.PaperFullDetectorMeasure.characterCoordinates_ne_zero_of_fullNonzero {χ : CharacterSpace} (hχ : χ ∈ fullNonzeroLocus) : PaperDualHaar.characterCoordinatesEquiv χ ≠ 0

A nonzero full character has a nonzero coordinate pair. Paper: §3 and §4.

theorem Connes.PaperFullDetectorMeasure.fullNonzeroLocus_subset_coordinate_loci (χ : CharacterSpace) (hχ : χ ∈ fullNonzeroLocus) : (∃ (v : SymplecticIndex), χ ∈ PaperAChartDetectorMeasure.aNonzeroLocus v) ∨ χ ∈ PaperChartDetectorMeasure.chartNonzeroLocus

def Connes.PaperFullDetectorMeasure.fullDetectorUnion : Set CharacterSpace

The fullDetectorUnion construction used in the Connes rigidity formalization.

Equations

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

theorem Connes.PaperFullDetectorMeasure.fullNonzeroLocus_subset_fullDetectorUnion : fullNonzeroLocus ⊆ fullDetectorUnion

theorem Connes.PaperFullDetectorMeasure.fullDetectorUnion_measureReal_le_five (μ : MeasureTheory.ProbabilityMeasure CharacterSpace) (hinv : PaperChartDetectorMeasure.IsInvariantPaperSL3SpectralMeasure μ) : (↑μ).real fullDetectorUnion ≤ 12 * (∑ v : SymplecticIndex, (↑μ).real (PaperAChartDetectorMeasure.aDetector v (PaperFiniteCharts.basisVector 0)) + (↑μ).real (PaperChartDetectorMeasure.chartDetector (Construction.PaperKernel.diagonal (PaperFiniteCharts.basisVector 0))))

theorem Connes.PaperFullDetectorMeasure.fullNonzeroLocus_measureReal_le_five (μ : MeasureTheory.ProbabilityMeasure CharacterSpace) (hinv : PaperChartDetectorMeasure.IsInvariantPaperSL3SpectralMeasure μ) : (↑μ).real fullNonzeroLocus ≤ 12 * (∑ v : SymplecticIndex, (↑μ).real (PaperAChartDetectorMeasure.aDetector v (PaperFiniteCharts.basisVector 0)) + (↑μ).real (PaperChartDetectorMeasure.chartDetector (Construction.PaperKernel.diagonal (PaperFiniteCharts.basisVector 0))))