Invariant dual-measure transport for Zhou's finite chart detector. Paper: §4.

@[reducible, inline]

abbrev Connes.PaperChartMeasure.k : Type

The k construction used in the Connes rigidity formalization.

Equations

• Connes.PaperChartMeasure.k = Connes.Construction.k

@[reducible, inline]

abbrev Connes.PaperChartMeasure.D : Type

The D construction used in the Connes rigidity formalization.

Equations

• Connes.PaperChartMeasure.D = Connes.Construction.PaperKernel.D

@[reducible, inline]

abbrev Connes.PaperChartMeasure.CharacterSpace : Type

The CharacterSpace construction used in the Connes rigidity formalization.

Equations

• Connes.PaperChartMeasure.CharacterSpace = Connes.PaperDualTopology.CharacterSpace

noncomputable def Connes.PaperChartMeasure.dualCharacterEquivOfAction {H : CountableDiscreteGroup} (action : H.Carrier →* Multiplicative (AddAut D)) (h : H.Carrier) : CharacterSpace ≃+ CharacterSpace

The dualCharacterEquivOfAction construction used in the Connes rigidity formalization.

Equations

• Connes.PaperChartMeasure.dualCharacterEquivOfAction action h = Connes.PaperDualAutomorphism.dualCharacterEquiv (Multiplicative.toAdd (action h))

noncomputable def Connes.PaperChartMeasure.paperDualCharacterAction {H : CountableDiscreteGroup} (action : H.Carrier →* Multiplicative (AddAut D)) (h : H.Carrier) : CharacterSpace → CharacterSpace

The paperDualCharacterAction construction used in the Connes rigidity formalization.

Equations

• Connes.PaperChartMeasure.paperDualCharacterAction action h = ⇑(Connes.PaperChartMeasure.dualCharacterEquivOfAction action h)

theorem Connes.PaperChartMeasure.continuous_paperDualCharacterAction {H : CountableDiscreteGroup} (action : H.Carrier →* Multiplicative (AddAut D)) (h : H.Carrier) : Continuous (paperDualCharacterAction action h)

The additive character action is continuous. Paper: §4.

theorem Connes.PaperChartMeasure.measurable_paperDualCharacterAction {H : CountableDiscreteGroup} (action : H.Carrier →* Multiplicative (AddAut D)) (h : H.Carrier) : Measurable (paperDualCharacterAction action h)

The additive character action is measurable. Paper: §4.

def Connes.PaperChartMeasure.IsInvariantPaperSpectralMeasure {H : CountableDiscreteGroup} (action : H.Carrier →* Multiplicative (AddAut D)) (μ : MeasureTheory.ProbabilityMeasure CharacterSpace) : Prop

Invariant probability measure for the additive character action, whose measurability is recorded above. Paper: §4.

Equations

• Connes.PaperChartMeasure.IsInvariantPaperSpectralMeasure action μ = ∀ (h : H.Carrier), MeasureTheory.Measure.map (Connes.PaperChartMeasure.paperDualCharacterAction action h) ↑μ = ↑μ

def Connes.PaperChartMeasure.linearDetector (d : D) : Set CharacterSpace

The linearDetector construction used in the Connes rigidity formalization.

Equations

• Connes.PaperChartMeasure.linearDetector d = {χ : Connes.PaperChartMeasure.CharacterSpace | (Connes.BinaryPontryaginDual.characterLinear (Additive.toMul χ)) d = 1}

theorem Connes.PaperChartMeasure.measurableSet_linearDetector (d : D) : MeasurableSet (linearDetector d)

theorem Connes.PaperChartMeasure.paperDualCharacterAction_preimage_linearDetector {H : CountableDiscreteGroup} (action : H.Carrier →* Multiplicative (AddAut D)) (h : H.Carrier) (d e : D) (he : (Multiplicative.toAdd (action h⁻¹)) e = d) : paperDualCharacterAction action h ⁻¹' linearDetector e = linearDetector d

theorem Connes.PaperChartMeasure.detector_measure_eq_of_invariant {H : CountableDiscreteGroup} (action : H.Carrier →* Multiplicative (AddAut D)) (μ : MeasureTheory.ProbabilityMeasure CharacterSpace) (hinv : IsInvariantPaperSpectralMeasure action μ) (h : H.Carrier) (d e : D) (he : (Multiplicative.toAdd (action h⁻¹)) e = d) : ↑μ (linearDetector e) = ↑μ (linearDetector d)