Concrete §4 chart detector transport and the invariant-measure bound for Zhou's dual kernel. Paper: §4.

@[reducible, inline]

abbrev Connes.PaperChartDetectorMeasure.k : Type

The k construction used in the Connes rigidity formalization.

Equations

• Connes.PaperChartDetectorMeasure.k = Connes.Construction.k

@[reducible, inline]

abbrev Connes.PaperChartDetectorMeasure.D : Type

The D construction used in the Connes rigidity formalization.

Equations

• Connes.PaperChartDetectorMeasure.D = Connes.Construction.PaperKernel.D

@[reducible, inline]

noncomputable abbrev Connes.PaperChartDetectorMeasure.H : CountableDiscreteGroup

The H construction used in the Connes rigidity formalization.

Equations

• Connes.PaperChartDetectorMeasure.H = Connes.Construction.actingGroup

@[reducible, inline]

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

The C construction used in the Connes rigidity formalization.

Equations

• Connes.PaperChartDetectorMeasure.C = Connes.Construction.PaperKernel.C

@[reducible, inline]

abbrev Connes.PaperChartDetectorMeasure.CharacterSpace : Type

The CharacterSpace construction used in the Connes rigidity formalization.

Equations

• Connes.PaperChartDetectorMeasure.CharacterSpace = Connes.PaperDualTopology.CharacterSpace

noncomputable def Connes.PaperChartDetectorMeasure.paperThetaOneAddAction : H.Carrier →* Multiplicative (AddAut D)

The paperThetaOneAddAction construction used in the Connes rigidity formalization.

Equations

• Connes.PaperChartDetectorMeasure.paperThetaOneAddAction = (MulAutMultiplicative Connes.PaperChartDetectorMeasure.D).toMonoidHom.comp Connes.Construction.PaperKernel.paperThetaOneHom

@[simp]

theorem Connes.PaperChartDetectorMeasure.paperThetaOneAddAction_apply (h : H.Carrier) (d : D) : (Multiplicative.toAdd (paperThetaOneAddAction h)) d = (Construction.PaperKernel.paperThetaOneLinear h) d

Pointwise form of the first Zhou action in the additive model.

noncomputable def Connes.PaperChartDetectorMeasure.paperThetaTwoAddAction : H.Carrier →* Multiplicative (AddAut D)

The second paper kernel action reserved for the companion detector. Paper: §4.

Equations

• Connes.PaperChartDetectorMeasure.paperThetaTwoAddAction = (MulAutMultiplicative Connes.PaperChartDetectorMeasure.D).toMonoidHom.comp Connes.Construction.PaperKernel.paperThetaTwoHom

@[simp]

theorem Connes.PaperChartDetectorMeasure.paperThetaTwoAddAction_apply (h : H.Carrier) (d : D) : (Multiplicative.toAdd (paperThetaTwoAddAction h)) d = (Construction.PaperKernel.paperThetaTwoLinearHom h) d

Pointwise form of the second Zhou action in the additive model.

def Connes.PaperChartDetectorMeasure.IsInvariantPaperSL3SpectralMeasure (μ : MeasureTheory.ProbabilityMeasure CharacterSpace) : Prop

In Zhou's detector corollary only the SL₃ subgroup is used. Paper: §4.

Equations

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

theorem Connes.PaperChartDetectorMeasure.IsInvariantPaperSL3SpectralMeasure.of_full (μ : MeasureTheory.ProbabilityMeasure CharacterSpace) (hinv : PaperChartMeasure.IsInvariantPaperSpectralMeasure paperThetaOneAddAction μ) : IsInvariantPaperSL3SpectralMeasure μ

Full acting-group invariance implies the SL₃ invariance needed by §4. Paper: §4.

theorem Connes.PaperChartDetectorMeasure.paperThetaOne_inverse_transport (g : SpecialLinear.SL3) (e : ↥C) (he : (Construction.PaperKernel.sl3CAction g) (Construction.PaperKernel.diagonal (PaperFiniteCharts.basisVector 0)) = e) : (Multiplicative.toAdd (paperThetaOneAddAction (g, 1)⁻¹)) (0, e) = (0, Construction.PaperKernel.diagonal (PaperFiniteCharts.basisVector 0))

noncomputable def Connes.PaperChartDetectorMeasure.chartLinear (χ : CharacterSpace) : ↥C →ₗ[k] k

The chartLinear construction used in the Connes rigidity formalization.

Equations

• Connes.PaperChartDetectorMeasure.chartLinear χ = (Connes.PaperDualHaar.characterCoordinatesEquiv χ).2

def Connes.PaperChartDetectorMeasure.chartDetector (c : ↥C) : Set CharacterSpace

The detector set associated with one C-coordinate. Paper: §4.

Equations

• Connes.PaperChartDetectorMeasure.chartDetector c = Connes.PaperChartMeasure.linearDetector (0, c)

theorem Connes.PaperChartDetectorMeasure.chartLinear_eval (χ : CharacterSpace) (c : ↥C) : (chartLinear χ) c = (BinaryPontryaginDual.characterLinear (Additive.toMul χ)) (0, c)

The C-coordinate agrees with direct character evaluation. Paper: §4.

theorem Connes.PaperChartDetectorMeasure.mem_chartDetector_iff (χ : CharacterSpace) (c : ↥C) : χ ∈ chartDetector c ↔ (chartLinear χ) c = 1

theorem Connes.PaperChartDetectorMeasure.detector_measure_eq_of_sl3_invariant (μ : MeasureTheory.ProbabilityMeasure CharacterSpace) (hinv : IsInvariantPaperSL3SpectralMeasure μ) (g : SpecialLinear.SL3) (d e : D) (he : (Multiplicative.toAdd (paperThetaOneAddAction (g, 1)⁻¹)) e = d) : ↑μ (PaperChartMeasure.linearDetector e) = ↑μ (PaperChartMeasure.linearDetector d)

theorem Connes.PaperChartDetectorMeasure.chartSquareDetector_measure_eq_base (μ : MeasureTheory.ProbabilityMeasure CharacterSpace) (hinv : IsInvariantPaperSL3SpectralMeasure μ) (N : ℕ) (i : PaperFiniteCharts.ChartIndex N) : ↑μ (chartDetector (PaperFiniteCharts.chartSquare N i)) = ↑μ (chartDetector (Construction.PaperKernel.diagonal (PaperFiniteCharts.basisVector 0)))

def Connes.PaperChartDetectorMeasure.chartEvalIndexEquiv (N : ℕ) : PaperFiniteCharts.ChartIndex N ≃ PaperChartDetector.ChartEvalIndex N

The chartEvalIndexEquiv construction used in the Connes rigidity formalization.

Equations

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

theorem Connes.PaperChartDetectorMeasure.chartIndexOfCoefficients_equiv (N : ℕ) (i : PaperFiniteCharts.ChartIndex N) : PaperChartDetector.chartIndexOfCoefficients N ((chartEvalIndexEquiv N) i).1 ((chartEvalIndexEquiv N) i).2 = i

Evaluation indices recover the original chart coefficients. Paper: §4.

theorem Connes.PaperChartDetectorMeasure.chartEvalValue_of_chartIndex (χ : CharacterSpace) (N : ℕ) (i : PaperFiniteCharts.ChartIndex N) : PaperChartDetector.chartEvalValue (chartLinear χ) N ((chartEvalIndexEquiv N) i) = (chartLinear χ) (PaperFiniteCharts.chartSquare N i)

noncomputable def Connes.PaperChartDetectorMeasure.chartDetectorSupport (χ : CharacterSpace) (N : ℕ) : Finset (PaperFiniteCharts.ChartIndex N)

The chartDetectorSupport construction used in the Connes rigidity formalization.

Equations

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

theorem Connes.PaperChartDetectorMeasure.chartDetectorSupport_mem_iff (χ : CharacterSpace) (N : ℕ) (i : PaperFiniteCharts.ChartIndex N) : i ∈ chartDetectorSupport χ N ↔ (chartEvalIndexEquiv N) i ∈ PaperChartDetector.chartEvalSupport (chartLinear χ) N

Active detector indices correspond exactly to nonzero chart evaluations. Paper: §4.

theorem Connes.PaperChartDetectorMeasure.chartDetectorSupport_card_eq (χ : CharacterSpace) (N : ℕ) : (chartDetectorSupport χ N).card = (PaperChartDetector.chartEvalSupport (chartLinear χ) N).card

theorem Connes.PaperChartDetectorMeasure.finite_detector_measure_bound {α : Type u_1} {I : Type u_2} [MeasurableSpace α] [Fintype I] [Nonempty I] (μ : MeasureTheory.Measure α) (family : I → Set α) (b : ENNReal) (hmeas : ∀ (i : I), MeasurableSet (family i)) (hcount : ∀ x ∈ ⋃ (i : I), family i, Fintype.card I ≤ 12 * Nat.card { i : I // x ∈ family i }) (hunif : ∀ (i : I), μ (family i) = b) : μ (⋃ (i : I), family i) ≤ 12 * b

theorem Connes.PaperChartDetectorMeasure.chartDetectorSupport_card_bound (χ : CharacterSpace) (N : ℕ) (hactive : (chartDetectorSupport χ N).Nonempty) : Fintype.card (PaperFiniteCharts.ChartIndex N) ≤ 12 * (chartDetectorSupport χ N).card

def Connes.PaperChartDetectorMeasure.chartDetectorUnion (N : ℕ) : Set CharacterSpace

The chartDetectorUnion construction used in the Connes rigidity formalization.

Equations

• Connes.PaperChartDetectorMeasure.chartDetectorUnion N = ⋃ (i : Connes.PaperFiniteCharts.ChartIndex N), Connes.PaperChartDetectorMeasure.chartDetector (Connes.PaperFiniteCharts.chartSquare N i)

theorem Connes.PaperChartDetectorMeasure.chartSquare_extend {N M : ℕ} (hNM : N ≤ M) (i : PaperFiniteCharts.ChartIndex N) : PaperFiniteCharts.chartSquare M (i.1, PaperFiniteCharts.extendCoefficients hNM i.2.1, PaperFiniteCharts.extendCoefficients hNM i.2.2) = PaperFiniteCharts.chartSquare N i

Extending polynomial coefficients preserves the represented chart square. Paper: §4.

theorem Connes.PaperChartDetectorMeasure.chartDetectorUnion_mono {N M : ℕ} (hNM : N ≤ M) : chartDetectorUnion N ⊆ chartDetectorUnion M

def Connes.PaperChartDetectorMeasure.chartNonzeroLocus : Set CharacterSpace

The chartNonzeroLocus construction used in the Connes rigidity formalization.

Equations

• Connes.PaperChartDetectorMeasure.chartNonzeroLocus = {χ : Connes.PaperChartDetectorMeasure.CharacterSpace | Connes.PaperChartDetectorMeasure.chartLinear χ ≠ 0}

theorem Connes.PaperChartDetectorMeasure.iUnion_chartDetectorUnion_eq_chartNonzeroLocus : ⋃ (N : ℕ), chartDetectorUnion N = chartNonzeroLocus

theorem Connes.PaperChartDetectorMeasure.measurableSet_chartDetectorUnion (N : ℕ) : MeasurableSet (chartDetectorUnion N)

theorem Connes.PaperChartDetectorMeasure.chartDetectorUnion_measure_le_twelve (μ : MeasureTheory.ProbabilityMeasure CharacterSpace) (hinv : IsInvariantPaperSL3SpectralMeasure μ) (N : ℕ) : ↑μ (chartDetectorUnion N) ≤ 12 * ↑μ (chartDetector (Construction.PaperKernel.diagonal (PaperFiniteCharts.basisVector 0)))

theorem Connes.PaperChartDetectorMeasure.chartNonzeroLocus_measureReal_le_twelve (μ : MeasureTheory.ProbabilityMeasure CharacterSpace) (hinv : IsInvariantPaperSL3SpectralMeasure μ) : (↑μ).real chartNonzeroLocus ≤ 12 * (↑μ).real (chartDetector (Construction.PaperKernel.diagonal (PaperFiniteCharts.basisVector 0)))