The dual shear measure component of the Connes rigidity formalization.

@[reducible, inline]

abbrev Connes.PaperDualShearMeasure.k : Type

The k construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualShearMeasure.k = Connes.Construction.k

@[reducible, inline]

abbrev Connes.PaperDualShearMeasure.Dadd : Type

The Dadd construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualShearMeasure.Dadd = Connes.Construction.PaperKernel.D

@[reducible, inline]

abbrev Connes.PaperDualShearMeasure.Padd : Type

The Padd construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualShearMeasure.Padd = Connes.Construction.PaperKernel.AVStar

@[reducible, inline]

abbrev Connes.PaperDualShearMeasure.Qadd : Submodule Construction.k Construction.PaperKernel.TensorAA

The Qadd construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualShearMeasure.Qadd = Connes.Construction.PaperKernel.C

@[reducible, inline]

abbrev Connes.PaperDualShearMeasure.D : Type

The D construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualShearMeasure.D = Multiplicative Connes.PaperDualShearMeasure.Dadd

@[reducible, inline]

abbrev Connes.PaperDualShearMeasure.P : Type

The P construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualShearMeasure.P = Multiplicative Connes.PaperDualShearMeasure.Padd

@[reducible, inline]

abbrev Connes.PaperDualShearMeasure.Q : Type

The Q construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualShearMeasure.Q = Multiplicative ↥Connes.PaperDualShearMeasure.Qadd

@[reducible, inline]

abbrev Connes.PaperDualShearMeasure.CharacterSpace : Type

The CharacterSpace construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualShearMeasure.CharacterSpace = Connes.PaperDualHaar.PaperCharacterSpace

@[instance_reducible]

noncomputable instance Connes.PaperDualShearMeasure.paperAVStarTopology : TopologicalSpace P

Equations

• Connes.PaperDualShearMeasure.paperAVStarTopology = ⊥

@[instance_reducible]

noncomputable instance Connes.PaperDualShearMeasure.paperCTopology : TopologicalSpace Q

Equations

• Connes.PaperDualShearMeasure.paperCTopology = ⊥

instance Connes.PaperDualShearMeasure.paperAVStarDiscrete : DiscreteTopology P

instance Connes.PaperDualShearMeasure.paperCDiscrete : DiscreteTopology Q

instance Connes.PaperDualShearMeasure.paperAVStarCountable : Countable P

instance Connes.PaperDualShearMeasure.paperCCountable : Countable Q

@[reducible, inline]

abbrev Connes.PaperDualShearMeasure.PChar : Type

The PChar construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualShearMeasure.PChar = PontryaginDual Connes.PaperDualShearMeasure.P

@[reducible, inline]

abbrev Connes.PaperDualShearMeasure.QChar : Type

The QChar construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualShearMeasure.QChar = PontryaginDual Connes.PaperDualShearMeasure.Q

instance Connes.PaperDualShearMeasure.paperAVCharSecondCountable : SecondCountableTopology PChar

instance Connes.PaperDualShearMeasure.paperCCharSecondCountable : SecondCountableTopology QChar

instance Connes.PaperDualShearMeasure.paperAVAdditiveSecondCountable : SecondCountableTopology (Additive PChar)

instance Connes.PaperDualShearMeasure.paperCAdditiveSecondCountable : SecondCountableTopology (Additive QChar)

@[instance_reducible]

noncomputable instance Connes.PaperDualShearMeasure.paperAVCharMeasurableSpace : MeasurableSpace (Additive PChar)

Equations

• Connes.PaperDualShearMeasure.paperAVCharMeasurableSpace = borel (Additive Connes.PaperDualShearMeasure.PChar)

instance Connes.PaperDualShearMeasure.paperAVCharBorelSpace : BorelSpace (Additive PChar)

@[instance_reducible]

noncomputable instance Connes.PaperDualShearMeasure.paperCCharMeasurableSpace : MeasurableSpace (Additive QChar)

Equations

• Connes.PaperDualShearMeasure.paperCCharMeasurableSpace = borel (Additive Connes.PaperDualShearMeasure.QChar)

instance Connes.PaperDualShearMeasure.paperCCharBorelSpace : BorelSpace (Additive QChar)

noncomputable def Connes.PaperDualShearMeasure.pInl : P →ₜ* D

The pInl construction used in the Connes rigidity formalization.

Equations

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

noncomputable def Connes.PaperDualShearMeasure.qInr : Q →ₜ* D

The qInr construction used in the Connes rigidity formalization.

Equations

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

def Connes.PaperDualShearMeasure.productToD : P × Q →ₜ* D

The productToD construction used in the Connes rigidity formalization.

Equations

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

def Connes.PaperDualShearMeasure.dToProduct : D →ₜ* P × Q

The dToProduct construction used in the Connes rigidity formalization.

Equations

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

@[simp]

theorem Connes.PaperDualShearMeasure.productToD_dToProduct (x : D) : productToD (dToProduct x) = x

@[simp]

theorem Connes.PaperDualShearMeasure.dToProduct_productToD (x : P × Q) : dToProduct (productToD x) = x

noncomputable def Connes.PaperDualShearMeasure.productToCharacter (p : Additive PChar × Additive QChar) : CharacterSpace

The actual dual is the product of the two compact summand duals. Paper: §3.

Equations

• Connes.PaperDualShearMeasure.productToCharacter p = Additive.ofMul ((ContinuousMonoidHom.coprod (Additive.toMul p.1) (Additive.toMul p.2)).comp Connes.PaperDualShearMeasure.dToProduct)

noncomputable def Connes.PaperDualShearMeasure.characterToProduct (χ : CharacterSpace) : Additive PChar × Additive QChar

The characterToProduct construction used in the Connes rigidity formalization.

Equations

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

noncomputable def Connes.PaperDualShearMeasure.characterProductEquiv : CharacterSpace ≃+ Additive PChar × Additive QChar

The characterProductEquiv construction used in the Connes rigidity formalization.

Equations

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

theorem Connes.PaperDualShearMeasure.continuous_characterToProduct : Continuous characterToProduct

theorem Connes.PaperDualShearMeasure.continuous_productToCharacter : Continuous productToCharacter

noncomputable def Connes.PaperDualShearMeasure.characterProductHomeomorph : CharacterSpace ≃ₜ Additive PChar × Additive QChar

The characterProductHomeomorph construction used in the Connes rigidity formalization.

Equations

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

noncomputable def Connes.PaperDualShearMeasure.productShear (p : Additive PChar × Additive QChar) : Additive PChar × Additive QChar

The compact dual shear and its product-coordinate form. Paper: §3.

Equations

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

theorem Connes.PaperDualShearMeasure.continuous_productShear : Continuous productShear

theorem Connes.PaperDualShearMeasure.productShear_first (p : Additive PChar × Additive QChar) : (productShear p).1 = p.1

theorem Connes.PaperDualShearMeasure.productCoordinate_first_eq (p : Additive PChar) (q : Additive QChar) : (PaperDualHaar.characterCoordinatesEquiv (productToCharacter (p, q))).1 = (PaperDualHaar.characterCoordinatesEquiv (productToCharacter (p, 0))).1

theorem Connes.PaperDualShearMeasure.productShear_second (p : Additive PChar) (q : Additive QChar) : (productShear (p, q)).2 = q + (productShear (p, 0)).2

noncomputable def Connes.PaperDualShearMeasure.productQuadraticCharacter (p : Additive PChar) : Additive QChar

The productQuadraticCharacter construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualShearMeasure.productQuadraticCharacter p = (Connes.PaperDualShearMeasure.productShear (p, 0)).2

theorem Connes.PaperDualShearMeasure.productShear_eq_skew (p : Additive PChar) (q : Additive QChar) : productShear (p, q) = (p, q + productQuadraticCharacter p)

theorem Connes.PaperDualShearMeasure.continuous_productQuadraticCharacter : Continuous productQuadraticCharacter

theorem Connes.PaperDualShearMeasure.productShear_measurePreserving : MeasureTheory.MeasurePreserving productShear (NormalizedHaar.productHaar (Additive PChar) (Additive QChar)) (NormalizedHaar.productHaar (Additive PChar) (Additive QChar))

theorem Connes.PaperDualShearMeasure.characterProductHaar_map : MeasureTheory.Measure.map (⇑characterProductEquiv) PaperDualHaar.paperCharacterHaar = NormalizedHaar.productHaar (Additive PChar) (Additive QChar)

@[reducible, inline]

abbrev Connes.PaperDualShearMeasure.Coordinates : Type

The Coordinates construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualShearMeasure.Coordinates = Connes.PaperFactorIsomorphism.DualCoordinates

noncomputable def Connes.PaperDualShearMeasure.coordinateProductEquiv : Coordinates ≃+ Additive PChar × Additive QChar

The coordinateProductEquiv construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualShearMeasure.coordinateProductEquiv = Connes.PaperDualHaar.characterCoordinatesEquiv.symm.trans Connes.PaperDualShearMeasure.characterProductEquiv

noncomputable def Connes.PaperDualShearMeasure.coordinateProductHomeomorph : Coordinates ≃ₜ Additive PChar × Additive QChar

The coordinateProductHomeomorph construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualShearMeasure.coordinateProductHomeomorph = Connes.PaperDualTopology.characterCoordinatesHomeomorph.symm.trans Connes.PaperDualShearMeasure.characterProductHomeomorph

instance Connes.PaperDualShearMeasure.coordinatesSecondCountable : SecondCountableTopology Coordinates

theorem Connes.PaperDualShearMeasure.coordinateProduct_shear_conj (p : Coordinates) : coordinateProductEquiv (PaperFactorIsomorphism.fiberShear p) = productShear (coordinateProductEquiv p)

theorem Connes.PaperDualShearMeasure.coordinateHaar_map : MeasureTheory.Measure.map (⇑coordinateProductEquiv) PaperDualTopology.coordinatesHaar = NormalizedHaar.productHaar (Additive PChar) (Additive QChar)

theorem Connes.PaperDualShearMeasure.fiberShear_measurePreserving : MeasureTheory.MeasurePreserving PaperFactorIsomorphism.fiberShear PaperDualTopology.coordinatesHaar PaperDualTopology.coordinatesHaar