The valued spectral measure component of the Connes rigidity formalization.

structure Connes.ProjectionValuedSpectralMeasure {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} [MeasurableSpace (DiscreteCharacterSpace A)] (E : SplitAbelianExtension A G H) (K : Type v) [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (π : UnitaryRepresentation G.Carrier K) : Type (max u v)

Projection-valued spectral data for a unitary representation. Paper: §4.

• projection : Set (DiscreteCharacterSpace A) → K →L[ℂ] K

  The projection component of ProjectionValuedSpectralMeasure.

• projection_empty : self.projection ∅ = 0
• projection_univ : self.projection Set.univ = 1
• projection_inter (s t : Set (DiscreteCharacterSpace A)) : MeasurableSet s → MeasurableSet t → self.projection (s ∩ t) = self.projection s ∘SL self.projection t
• projection_self_adjoint (s : Set (DiscreteCharacterSpace A)) : MeasurableSet s → ∀ (x y : K), inner ℂ ((self.projection s) x) y = inner ℂ x ((self.projection s) y)
• projection_iUnion (s : ℕ → Set (DiscreteCharacterSpace A)) : (∀ (n : ℕ), MeasurableSet (s n)) → (∀ (i j : ℕ), i ≠ j → Disjoint (s i) (s j)) → ∀ (x : K), HasSum (fun (n : ℕ) => (self.projection (s n)) x) ((self.projection (⋃ (n : ℕ), s n)) x)
• scalar : K → MeasureTheory.Measure (DiscreteCharacterSpace A)

  The scalar component of ProjectionValuedSpectralMeasure.

• scalar_apply (x : K) (s : Set (DiscreteCharacterSpace A)) : MeasurableSet s → (self.scalar x).real s = (inner ℂ x ((self.projection s) x)).re
• projection_covariance (h : H.Carrier) (s : Set (DiscreteCharacterSpace A)) (x : K) : ↑(π (E.splitting h)) ((self.projection s) x) = (self.projection (dualCharacterAction E.action h '' s)) (↑(π (E.splitting h)) x)
• scalar_covariance (h : H.Carrier) (x : K) : MeasureTheory.Measure.map (dualCharacterAction E.action h) (self.scalar x) = self.scalar (↑(π (E.splitting h)) x)
• kernel_eigenprojection (a : A) (χ : DiscreteCharacterSpace A) (x : K) : ↑(π (E.inclusion (Multiplicative.ofAdd a))) ((self.projection {χ}) x) = ↑(χ (Multiplicative.ofAdd a)) • (self.projection {χ}) x
• energy_identity (x : K) (a : A) : ∫ (χ : DiscreteCharacterSpace A), ‖↑(χ (Multiplicative.ofAdd a)) - 1‖ ^ 2 ∂self.scalar x = ‖↑(π (E.inclusion (Multiplicative.ofAdd a))) x - x‖ ^ 2

theorem Connes.ProjectionValuedSpectralMeasure.scalar_univ_real {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} [MeasurableSpace (DiscreteCharacterSpace A)] {E : SplitAbelianExtension A G H} {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {π : UnitaryRepresentation G.Carrier K} (P : ProjectionValuedSpectralMeasure E K π) (x : K) : (P.scalar x).real Set.univ = ‖x‖ ^ 2

The scalar spectral measure has total mass equal to squared norm. Paper: §4.

theorem Connes.ProjectionValuedSpectralMeasure.scalar_isProbabilityMeasure {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} [MeasurableSpace (DiscreteCharacterSpace A)] {E : SplitAbelianExtension A G H} {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {π : UnitaryRepresentation G.Carrier K} (P : ProjectionValuedSpectralMeasure E K π) (x : K) (hx : ‖x‖ = 1) : MeasureTheory.IsProbabilityMeasure (P.scalar x)

A unit vector normalizes its scalar spectral measure. Paper: §4.

def Connes.ProjectionValuedSpectralMeasure.probabilityMeasure {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} [MeasurableSpace (DiscreteCharacterSpace A)] {E : SplitAbelianExtension A G H} {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {π : UnitaryRepresentation G.Carrier K} (P : ProjectionValuedSpectralMeasure E K π) (x : K) (hx : ‖x‖ = 1) : MeasureTheory.ProbabilityMeasure (DiscreteCharacterSpace A)

Package a unit vector's scalar measure as a probability measure. Paper: §4.

Equations

• P.probabilityMeasure x hx = ⟨P.scalar x, ⋯⟩

theorem Connes.ProjectionValuedSpectralMeasure.probabilityMeasure_invariant {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} [MeasurableSpace (DiscreteCharacterSpace A)] {E : SplitAbelianExtension A G H} {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {π : UnitaryRepresentation G.Carrier K} (P : ProjectionValuedSpectralMeasure E K π) (x : QuotientFixedUnitVector E K π) : IsInvariantSpectralMeasure E.action (P.probabilityMeasure x.vector ⋯)

Quotient-fixed vectors produce invariant scalar spectral measures. Paper: §4.

theorem Connes.ProjectionValuedSpectralMeasure.probabilityMeasure_energy {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} [MeasurableSpace (DiscreteCharacterSpace A)] {E : SplitAbelianExtension A G H} {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {π : UnitaryRepresentation G.Carrier K} (P : ProjectionValuedSpectralMeasure E K π) (x : QuotientFixedUnitVector E K π) (a : A) : spectralDetectionEnergy (P.probabilityMeasure x.vector ⋯) a = ‖↑(π (E.inclusion (Multiplicative.ofAdd a))) x.vector - x.vector‖ ^ 2

The scalar spectral energy is the kernel displacement energy. Paper: §4.

theorem Connes.ProjectionValuedSpectralMeasure.trivialProjection_ne_zero_of_atom_pos {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} [MeasurableSpace (DiscreteCharacterSpace A)] [MeasurableSingletonClass (DiscreteCharacterSpace A)] {E : SplitAbelianExtension A G H} {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {π : UnitaryRepresentation G.Carrier K} (P : ProjectionValuedSpectralMeasure E K π) (x : QuotientFixedUnitVector E K π) (hx : 0 < spectralTrivialAtom (P.probabilityMeasure x.vector ⋯)) : (P.projection {1}) x.vector ≠ 0

A positive trivial atom gives a nonzero trivial spectral projection. Paper: §4.

theorem Connes.ProjectionValuedSpectralMeasure.trivialProjection_kernel_fixed {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} [MeasurableSpace (DiscreteCharacterSpace A)] {E : SplitAbelianExtension A G H} {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {π : UnitaryRepresentation G.Carrier K} (P : ProjectionValuedSpectralMeasure E K π) (x : K) (a : A) : ↑(π (E.inclusion (Multiplicative.ofAdd a))) ((P.projection {1}) x) = (P.projection {1}) x

The trivial spectral projection is fixed by every kernel element. Paper: §4.

theorem Connes.ProjectionValuedSpectralMeasure.trivialProjection_quotient_fixed {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} [MeasurableSpace (DiscreteCharacterSpace A)] {E : SplitAbelianExtension A G H} {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {π : UnitaryRepresentation G.Carrier K} (P : ProjectionValuedSpectralMeasure E K π) (x : QuotientFixedUnitVector E K π) (h : H.Carrier) : ↑(π (E.splitting h)) ((P.projection {1}) x.vector) = (P.projection {1}) x.vector

The trivial spectral projection is fixed by every quotient section. Paper: §4.

theorem Connes.ProjectionValuedSpectralMeasure.positive_atom_invariant {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} [MeasurableSpace (DiscreteCharacterSpace A)] [MeasurableSingletonClass (DiscreteCharacterSpace A)] {E : SplitAbelianExtension A G H} {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {π : UnitaryRepresentation G.Carrier K} (P : ProjectionValuedSpectralMeasure E K π) (x : QuotientFixedUnitVector E K π) (hx : 0 < spectralTrivialAtom (P.probabilityMeasure x.vector ⋯)) : ∃ (η : K), η ≠ 0 ∧ (∀ (a : A), ↑(π (E.inclusion (Multiplicative.ofAdd a))) η = η) ∧ ∀ (h : H.Carrier), ↑(π (E.splitting h)) η = η

A positive trivial atom yields a vector fixed by the split extension. Paper: §4.

def Connes.ProjectionValuedSpectralMeasure.HasQuotientFixedApproximation {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier K) : Prop

The HasQuotientFixedApproximation construction used in the Connes rigidity formalization.

Equations

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

theorem Connes.ProjectionValuedSpectralMeasure.exists_quotientFixedUnitVector_with_displacement {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} {E : SplitAbelianExtension A G H} {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {π : UnitaryRepresentation G.Carrier K} (hH : HasKazhdanPropertyT H) (hπ : π.HasAlmostInvariantUnitVectors) (T : Finset G.Carrier) (ε : ℝ) (hε : 0 < ε) : ∃ (x : QuotientFixedUnitVector E K π), ∀ g ∈ T, ‖↑(π g) x.vector - x.vector‖ < ε

theorem Connes.ProjectionValuedSpectralMeasure.hasQuotientFixedApproximation {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} {E : SplitAbelianExtension A G H} {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {π : UnitaryRepresentation G.Carrier K} : HasQuotientFixedApproximation E π

def Connes.ProjectionValuedSpectralMeasure.toSpectralMeasureInterface {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} [MeasurableSpace (DiscreteCharacterSpace A)] [MeasurableSingletonClass (DiscreteCharacterSpace A)] {E : SplitAbelianExtension A G H} {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {π : UnitaryRepresentation G.Carrier K} (P : ProjectionValuedSpectralMeasure E K π) (approximation : HasQuotientFixedApproximation E π) : SpectralMeasureInterface E K π

Convert a PVM and quotient approximation into the generic spectral interface. Paper: §4.

Equations

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

theorem Connes.relative_propertyT_of_projectionValuedSpectralMeasure {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} [MeasurableSpace (DiscreteCharacterSpace A)] [MeasurableSingletonClass (DiscreteCharacterSpace A)] (E : SplitAbelianExtension A G H) (hH : HasKazhdanPropertyT H) (J : Finset A) {c : ℝ} (hc : 0 < c) (hdetection : HasFiniteSpectralDetection E J c) (pvm : (K : Type v) → (x : NormedAddCommGroup K) → (x_1 : InnerProductSpace ℂ K) → (x_2 : CompleteSpace K) → (π : UnitaryRepresentation G.Carrier K) → ProjectionValuedSpectralMeasure E K π) : HasKazhdanPropertyT G

Relative property-(T) from an analytic PVM and detector. Quotient approximation follows generically from quotient property (T). Paper: §4.