The normalized haar component of the Connes rigidity formalization.

noncomputable def Connes.NormalizedHaar.normalizedAddHaar (A : Type u) [AddGroup A] [TopologicalSpace A] [CompactSpace A] [IsTopologicalAddGroup A] [MeasurableSpace A] [BorelSpace A] : MeasureTheory.Measure A

The probability normalization of additive Haar measure on a compact group. Paper: §3.

Equations

• Connes.NormalizedHaar.normalizedAddHaar A = MeasureTheory.Measure.addHaarMeasure { carrier := Set.univ, isCompact' := ⋯, interior_nonempty' := ⋯ }

instance Connes.NormalizedHaar.normalizedAddHaar_isProbabilityMeasure (A : Type u) [AddGroup A] [TopologicalSpace A] [CompactSpace A] [IsTopologicalAddGroup A] [MeasurableSpace A] [BorelSpace A] : MeasureTheory.IsProbabilityMeasure (normalizedAddHaar A)

instance Connes.NormalizedHaar.normalizedAddHaar_isAddHaarMeasure (A : Type u) [AddGroup A] [TopologicalSpace A] [CompactSpace A] [IsTopologicalAddGroup A] [MeasurableSpace A] [BorelSpace A] : (normalizedAddHaar A).IsAddHaarMeasure

theorem Connes.NormalizedHaar.normalizedAddHaar_unique (A : Type u) [AddGroup A] [TopologicalSpace A] [CompactSpace A] [IsTopologicalAddGroup A] [SecondCountableTopology A] [MeasurableSpace A] [BorelSpace A] (μ : MeasureTheory.Measure A) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] : μ = normalizedAddHaar A

Probability-normalized additive Haar measure is unique. Paper: §3.

theorem Connes.NormalizedHaar.normalizedAddHaar_preserving_addEquiv (A : Type u) [AddCommGroup A] [TopologicalSpace A] [CompactSpace A] [IsTopologicalAddGroup A] [SecondCountableTopology A] [MeasurableSpace A] [BorelSpace A] (e : A ≃+ A) (he : Continuous ⇑e) (heinv : Continuous ⇑e.symm) : MeasureTheory.MeasurePreserving (⇑e) (normalizedAddHaar A) (normalizedAddHaar A)

Continuous additive automorphisms preserve normalized Haar measure. Paper: §3.

theorem Connes.NormalizedHaar.skew_add_translation_measurePreserving {P : Type u} {Q : Type v} [AddCommGroup P] [AddCommGroup Q] [TopologicalSpace P] [TopologicalSpace Q] [IsTopologicalAddGroup P] [IsTopologicalAddGroup Q] [SecondCountableTopology Q] [MeasurableSpace P] [BorelSpace P] [MeasurableSpace Q] [BorelSpace Q] (μ : MeasureTheory.Measure P) (ν : MeasureTheory.Measure Q) [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] [μ.IsAddLeftInvariant] [ν.IsAddLeftInvariant] (a : P) (b : Q) (c : P → Q) (hc : Continuous c) : MeasureTheory.MeasurePreserving (fun (z : P × Q) => (a + z.1, b + z.2 + c z.1)) (μ.prod ν) (μ.prod ν)

A continuous fiber shear by an additive term preserves product Haar measure. Paper: §3.

noncomputable def Connes.NormalizedHaar.productHaar (P : Type u) (Q : Type v) [AddGroup P] [AddGroup Q] [TopologicalSpace P] [TopologicalSpace Q] [CompactSpace P] [CompactSpace Q] [IsTopologicalAddGroup P] [IsTopologicalAddGroup Q] [MeasurableSpace P] [BorelSpace P] [MeasurableSpace Q] [BorelSpace Q] : MeasureTheory.Measure (P × Q)

Product probability Haar measure for two compact additive groups. Paper: §3.

Equations

• Connes.NormalizedHaar.productHaar P Q = (Connes.NormalizedHaar.normalizedAddHaar P).prod (Connes.NormalizedHaar.normalizedAddHaar Q)

instance Connes.NormalizedHaar.productHaar_isProbabilityMeasure (P : Type u) (Q : Type v) [AddGroup P] [AddGroup Q] [TopologicalSpace P] [TopologicalSpace Q] [CompactSpace P] [CompactSpace Q] [IsTopologicalAddGroup P] [IsTopologicalAddGroup Q] [MeasurableSpace P] [BorelSpace P] [MeasurableSpace Q] [BorelSpace Q] : MeasureTheory.IsProbabilityMeasure (productHaar P Q)

instance Connes.NormalizedHaar.productHaar_isAddLeftInvariant (P : Type u) (Q : Type v) [AddCommGroup P] [AddCommGroup Q] [TopologicalSpace P] [TopologicalSpace Q] [CompactSpace P] [CompactSpace Q] [IsTopologicalAddGroup P] [IsTopologicalAddGroup Q] [MeasurableSpace P] [BorelSpace P] [MeasurableSpace Q] [BorelSpace Q] : (productHaar P Q).IsAddLeftInvariant

theorem Connes.NormalizedHaar.productHaar_eq_normalizedAddHaar (P : Type u) (Q : Type v) [AddCommGroup P] [AddCommGroup Q] [TopologicalSpace P] [TopologicalSpace Q] [CompactSpace P] [CompactSpace Q] [IsTopologicalAddGroup P] [IsTopologicalAddGroup Q] [SecondCountableTopology P] [SecondCountableTopology Q] [MeasurableSpace P] [BorelSpace P] [MeasurableSpace Q] [BorelSpace Q] : productHaar P Q = normalizedAddHaar (P × Q)

The product measure agrees with normalized Haar measure on the product group. Paper: §3.

theorem Connes.NormalizedHaar.productHaar_preserving_addEquiv (P : Type u) (Q : Type v) [AddCommGroup P] [AddCommGroup Q] [TopologicalSpace P] [TopologicalSpace Q] [CompactSpace P] [CompactSpace Q] [IsTopologicalAddGroup P] [IsTopologicalAddGroup Q] [SecondCountableTopology P] [SecondCountableTopology Q] [MeasurableSpace P] [BorelSpace P] [MeasurableSpace Q] [BorelSpace Q] (e : P × Q ≃+ P × Q) (he : Continuous ⇑e) (heinv : Continuous ⇑e.symm) : MeasureTheory.MeasurePreserving (⇑e) (productHaar P Q) (productHaar P Q)

Continuous additive automorphisms of a product preserve product Haar. Paper: §3.