The positive spectral measure component of the Connes rigidity formalization.

def Connes.spectralUnitTest (A : Type u) [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] : CompactlySupportedContinuousMap (DiscreteCharacterSpace A) ℝ

The spectralUnitTest construction used in the Connes rigidity formalization.

Equations

• Connes.spectralUnitTest A = { toFun := fun (x : Connes.DiscreteCharacterSpace A) => 1, continuous_toFun := ⋯, hasCompactSupport' := ⋯ }

@[simp]

theorem Connes.spectralUnitTest_apply {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] (χ : DiscreteCharacterSpace A) : (spectralUnitTest A) χ = 1

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

A positive spectral functional associated with a unitary representation.

• functional : V → CompactlySupportedContinuousMap (DiscreteCharacterSpace A) ℝ →ₚ[ℝ] ℝ

  The functional component of PositiveSpectralFunctional.

• normalization (x : V) : (self.functional x) (spectralUnitTest A) = ‖x‖ ^ 2
• energy (x : V) (a : A) : (self.functional x) (spectralEnergyTest a) = ‖↑(π (E.inclusion (Multiplicative.ofAdd a))) x - x‖ ^ 2
• covariance (h : H.Carrier) (x : V) : MeasureTheory.Measure.map (dualCharacterAction E.action h) (RealRMK.rieszMeasure (self.functional x)) = RealRMK.rieszMeasure (self.functional (↑(π (E.splitting h)) x))

noncomputable def Connes.PositiveSpectralFunctional.measure {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} [MeasurableSpace (DiscreteCharacterSpace A)] [BorelSpace (DiscreteCharacterSpace A)] {E : SplitAbelianExtension A G H} {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] {π : UnitaryRepresentation G.Carrier V} (Φ : PositiveSpectralFunctional E V π) (x : V) : MeasureTheory.Measure (DiscreteCharacterSpace A)

The measure construction used in the Connes rigidity formalization.

Equations

• Φ.measure x = RealRMK.rieszMeasure (Φ.functional x)

instance Connes.PositiveSpectralFunctional.measure_regular {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} [MeasurableSpace (DiscreteCharacterSpace A)] [BorelSpace (DiscreteCharacterSpace A)] {E : SplitAbelianExtension A G H} {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] {π : UnitaryRepresentation G.Carrier V} (Φ : PositiveSpectralFunctional E V π) (x : V) : (Φ.measure x).Regular

instance Connes.PositiveSpectralFunctional.measure_isFiniteMeasure {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} [MeasurableSpace (DiscreteCharacterSpace A)] [BorelSpace (DiscreteCharacterSpace A)] {E : SplitAbelianExtension A G H} {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] {π : UnitaryRepresentation G.Carrier V} (Φ : PositiveSpectralFunctional E V π) (x : V) : MeasureTheory.IsFiniteMeasure (Φ.measure x)

theorem Connes.PositiveSpectralFunctional.integral_measure {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} [MeasurableSpace (DiscreteCharacterSpace A)] [BorelSpace (DiscreteCharacterSpace A)] {E : SplitAbelianExtension A G H} {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] {π : UnitaryRepresentation G.Carrier V} (Φ : PositiveSpectralFunctional E V π) (x : V) (f : CompactlySupportedContinuousMap (DiscreteCharacterSpace A) ℝ) : ∫ (χ : DiscreteCharacterSpace A), f χ ∂Φ.measure x = (Φ.functional x) f

theorem Connes.PositiveSpectralFunctional.measure_univ_real {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} [MeasurableSpace (DiscreteCharacterSpace A)] [BorelSpace (DiscreteCharacterSpace A)] {E : SplitAbelianExtension A G H} {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] {π : UnitaryRepresentation G.Carrier V} (Φ : PositiveSpectralFunctional E V π) (x : V) : (Φ.measure x).real Set.univ = ‖x‖ ^ 2

theorem Connes.PositiveSpectralFunctional.measure_isProbabilityMeasure {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} [MeasurableSpace (DiscreteCharacterSpace A)] [BorelSpace (DiscreteCharacterSpace A)] {E : SplitAbelianExtension A G H} {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] {π : UnitaryRepresentation G.Carrier V} (Φ : PositiveSpectralFunctional E V π) (x : V) (hx : ‖x‖ = 1) : MeasureTheory.IsProbabilityMeasure (Φ.measure x)

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

The probabilityMeasure construction used in the Connes rigidity formalization.

Equations

• Φ.probabilityMeasure x hx = ⟨Φ.measure x, ⋯⟩

@[simp]

theorem Connes.PositiveSpectralFunctional.probabilityMeasure_toMeasure {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} [MeasurableSpace (DiscreteCharacterSpace A)] [BorelSpace (DiscreteCharacterSpace A)] {E : SplitAbelianExtension A G H} {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] {π : UnitaryRepresentation G.Carrier V} (Φ : PositiveSpectralFunctional E V π) (x : V) (hx : ‖x‖ = 1) : ↑(Φ.probabilityMeasure x hx) = Φ.measure x

theorem Connes.PositiveSpectralFunctional.measure_energy {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} [MeasurableSpace (DiscreteCharacterSpace A)] [BorelSpace (DiscreteCharacterSpace A)] {E : SplitAbelianExtension A G H} {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] {π : UnitaryRepresentation G.Carrier V} (Φ : PositiveSpectralFunctional E V π) (x : V) (a : A) : ∫ (χ : DiscreteCharacterSpace A), ‖↑(χ (Multiplicative.ofAdd a)) - 1‖ ^ 2 ∂Φ.measure x = ‖↑(π (E.inclusion (Multiplicative.ofAdd a))) x - x‖ ^ 2

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

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

noncomputable def Connes.kernelFixedSubmodule {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} (E : SplitAbelianExtension A G H) {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (π : UnitaryRepresentation G.Carrier V) : Submodule ℂ V

The kernelFixedSubmodule construction used in the Connes rigidity formalization.

Equations

• Connes.kernelFixedSubmodule E π = ⨅ (a : A), (↑(↑(π (E.inclusion (Multiplicative.ofAdd a))) - ContinuousLinearMap.id ℂ V)).ker

theorem Connes.mem_kernelFixedSubmodule {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} (E : SplitAbelianExtension A G H) {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (π : UnitaryRepresentation G.Carrier V) (x : V) : x ∈ kernelFixedSubmodule E π ↔ ∀ (a : A), ↑(π (E.inclusion (Multiplicative.ofAdd a))) x = x

theorem Connes.kernelFixedSubmodule_isClosed {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} (E : SplitAbelianExtension A G H) {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (π : UnitaryRepresentation G.Carrier V) : IsClosed ↑(kernelFixedSubmodule E π)

instance Connes.kernelFixedSubmodule_completeSpace {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} (E : SplitAbelianExtension A G H) {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (π : UnitaryRepresentation G.Carrier V) : CompleteSpace ↥(kernelFixedSubmodule E π)

noncomputable def Connes.trivialCharacterProjection {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} (E : SplitAbelianExtension A G H) {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (π : UnitaryRepresentation G.Carrier V) : V →L[ℂ] V

The trivialCharacterProjection construction used in the Connes rigidity formalization.

Equations

• Connes.trivialCharacterProjection E π = (Connes.kernelFixedSubmodule E π).starProjection

theorem Connes.trivialCharacterProjection_kernel_fixed {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} (E : SplitAbelianExtension A G H) {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (π : UnitaryRepresentation G.Carrier V) (x : V) (a : A) : ↑(π (E.inclusion (Multiplicative.ofAdd a))) ((trivialCharacterProjection E π) x) = (trivialCharacterProjection E π) x

theorem Connes.kernel_map_kernelFixedSubmodule {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} (E : SplitAbelianExtension A G H) {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (π : UnitaryRepresentation G.Carrier V) (a : A) : Submodule.map (↑(Unitary.linearIsometryEquiv (π (E.inclusion (Multiplicative.ofAdd a)))).toLinearEquiv) (kernelFixedSubmodule E π) = kernelFixedSubmodule E π

theorem Connes.trivialCharacterProjection_kernel_commutes {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} (E : SplitAbelianExtension A G H) {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (π : UnitaryRepresentation G.Carrier V) (a : A) (x : V) : ↑(π (E.inclusion (Multiplicative.ofAdd a))) ((trivialCharacterProjection E π) x) = (trivialCharacterProjection E π) (↑(π (E.inclusion (Multiplicative.ofAdd a))) x)

theorem Connes.trivialCharacterProjection_kernel_orbit {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} (E : SplitAbelianExtension A G H) {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (π : UnitaryRepresentation G.Carrier V) (a : A) (x : V) : (trivialCharacterProjection E π) (↑(π (E.inclusion (Multiplicative.ofAdd a))) x) = (trivialCharacterProjection E π) x

theorem Connes.quotient_preserves_kernelFixedSubmodule {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} (E : SplitAbelianExtension A G H) {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (π : UnitaryRepresentation G.Carrier V) (h : H.Carrier) {x : V} (hx : x ∈ kernelFixedSubmodule E π) : ↑(π (E.splitting h)) x ∈ kernelFixedSubmodule E π

theorem Connes.quotient_map_kernelFixedSubmodule {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} (E : SplitAbelianExtension A G H) {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (π : UnitaryRepresentation G.Carrier V) (h : H.Carrier) : Submodule.map (↑(Unitary.linearIsometryEquiv (π (E.splitting h))).toLinearEquiv) (kernelFixedSubmodule E π) = kernelFixedSubmodule E π

theorem Connes.trivialCharacterProjection_quotient_commutes {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} (E : SplitAbelianExtension A G H) {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (π : UnitaryRepresentation G.Carrier V) (h : H.Carrier) (x : V) : ↑(π (E.splitting h)) ((trivialCharacterProjection E π) x) = (trivialCharacterProjection E π) (↑(π (E.splitting h)) x)

theorem Connes.measureReal_singleton_le_integral_of_nonneg {Ω : Type v} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] (μ : MeasureTheory.Measure Ω) (f : Ω → ℝ) (x : Ω) (hf : MeasureTheory.Integrable f μ) (hpos : ∀ (y : Ω), 0 ≤ f y) (hone : 1 ≤ f x) : μ.real {x} ≤ ∫ (y : Ω), f y ∂μ

theorem Connes.PositiveSpectralFunctional.trivial_atom_le_functional_of_nonneg {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} [MeasurableSpace (DiscreteCharacterSpace A)] [BorelSpace (DiscreteCharacterSpace A)] {W : Type w} [NormedAddCommGroup W] [InnerProductSpace ℂ W] [CompleteSpace W] {E : SplitAbelianExtension A G H} {π : UnitaryRepresentation G.Carrier W} (Φ : PositiveSpectralFunctional E W π) (x : W) (f : CompactlySupportedContinuousMap (DiscreteCharacterSpace A) ℝ) (hpos : ∀ (χ : DiscreteCharacterSpace A), 0 ≤ f χ) (hone : 1 ≤ f 1) : (Φ.measure x).real {1} ≤ (Φ.functional x) f

theorem Connes.kernel_orbit_sub_norm {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} {W : Type w} [NormedAddCommGroup W] [InnerProductSpace ℂ W] [CompleteSpace W] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier W) (x : W) (a b : A) : ‖↑(π (E.inclusion (Multiplicative.ofAdd a))) x - ↑(π (E.inclusion (Multiplicative.ofAdd b))) x‖ = ‖↑(π (E.inclusion (Multiplicative.ofAdd (a - b)))) x - x‖

theorem Connes.kernel_orbit_sub_norm_sq {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} {W : Type w} [NormedAddCommGroup W] [InnerProductSpace ℂ W] [CompleteSpace W] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier W) (x : W) (a b : A) : ‖↑(π (E.inclusion (Multiplicative.ofAdd a))) x - ↑(π (E.inclusion (Multiplicative.ofAdd b))) x‖ ^ 2 = ‖↑(π (E.inclusion (Multiplicative.ofAdd (a - b)))) x - x‖ ^ 2

theorem Connes.character_sub_norm {A : Type u} [AddCommGroup A] [TopologicalSpace A] (χ : DiscreteCharacterSpace A) (a b : A) : ‖↑(χ (Multiplicative.ofAdd a)) - ↑(χ (Multiplicative.ofAdd b))‖ = ‖↑(χ (Multiplicative.ofAdd (a - b))) - 1‖

theorem Connes.character_sub_norm_sq {A : Type u} [AddCommGroup A] [TopologicalSpace A] (χ : DiscreteCharacterSpace A) (a b : A) : ‖↑(χ (Multiplicative.ofAdd a)) - ↑(χ (Multiplicative.ofAdd b))‖ ^ 2 = ‖↑(χ (Multiplicative.ofAdd (a - b))) - 1‖ ^ 2

noncomputable def Connes.spectralFiniteAverageTest {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {ι : Type v} (s : Finset ι) (a : ι → A) (w : ι → ℝ) : CompactlySupportedContinuousMap (DiscreteCharacterSpace A) ℝ

The spectralFiniteAverageTest construction used in the Connes rigidity formalization.

Equations

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

@[simp]

theorem Connes.spectralFiniteAverageTest_apply {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {ι : Type v} (s : Finset ι) (a : ι → A) (w : ι → ℝ) (χ : DiscreteCharacterSpace A) : (spectralFiniteAverageTest s a w) χ = ‖∑ i ∈ s, ↑(w i) * ↑(χ (Multiplicative.ofAdd (a i)))‖ ^ 2

theorem Connes.spectralFiniteAverageTest_nonneg {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {ι : Type v} (s : Finset ι) (a : ι → A) (w : ι → ℝ) (χ : DiscreteCharacterSpace A) : 0 ≤ (spectralFiniteAverageTest s a w) χ

theorem Connes.spectralFiniteAverageTest_one {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {ι : Type v} (s : Finset ι) (a : ι → A) (w : ι → ℝ) (hw : ∑ i ∈ s, w i = 1) : (spectralFiniteAverageTest s a w) 1 = 1

theorem Connes.PositiveSpectralFunctional.trivial_atom_le_finiteAverage_functional {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} [MeasurableSpace (DiscreteCharacterSpace A)] [BorelSpace (DiscreteCharacterSpace A)] {W : Type w} [NormedAddCommGroup W] [InnerProductSpace ℂ W] [CompleteSpace W] {E : SplitAbelianExtension A G H} {π : UnitaryRepresentation G.Carrier W} (Φ : PositiveSpectralFunctional E W π) (x : W) {ι : Type v} (s : Finset ι) (a : ι → A) (w : ι → ℝ) (hw : ∑ i ∈ s, w i = 1) : (Φ.measure x).real {1} ≤ (Φ.functional x) (spectralFiniteAverageTest s a w)

theorem Connes.weighted_norm_sq_eq_sub_pairwise_dist_sq {ι : Type u_1} {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (s : Finset ι) (w : ι → ℝ) (v : ι → V) (hw : ∑ i ∈ s, w i = 1) : ‖∑ i ∈ s, w i • v i‖ ^ 2 = ∑ i ∈ s, w i * ‖v i‖ ^ 2 - 1 / 2 * ∑ i ∈ s, ∑ j ∈ s, w i * w j * ‖v i - v j‖ ^ 2

theorem Connes.weighted_norm_sq_eq_sub_pairwise_dist_sq_of_constant_norm {ι : Type u_1} {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (s : Finset ι) (w : ι → ℝ) (v : ι → V) (r : ℝ) (hw : ∑ i ∈ s, w i = 1) (hv : ∀ i ∈ s, ‖v i‖ = r) : ‖∑ i ∈ s, w i • v i‖ ^ 2 = r ^ 2 - 1 / 2 * ∑ i ∈ s, ∑ j ∈ s, w i * w j * ‖v i - v j‖ ^ 2

theorem Connes.spectralFiniteAverageTest_eq_sub_energy {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {ι : Type u_1} (s : Finset ι) (a : ι → A) (w : ι → ℝ) (hw : ∑ i ∈ s, w i = 1) : spectralFiniteAverageTest s a w = spectralUnitTest A - (1 / 2) • ∑ i ∈ s, ∑ j ∈ s, (w i * w j) • spectralEnergyTest (a i - a j)

theorem Connes.PositiveSpectralFunctional.finiteAverage_functional_eq_kernel_orbit_norm_sq {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} [MeasurableSpace (DiscreteCharacterSpace A)] [BorelSpace (DiscreteCharacterSpace A)] {E : SplitAbelianExtension A G H} {V : Type w} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] {π : UnitaryRepresentation G.Carrier V} (Φ : PositiveSpectralFunctional E V π) (x : V) {ι : Type u_1} (s : Finset ι) (a : ι → A) (w : ι → ℝ) (hw : ∑ i ∈ s, w i = 1) : (Φ.functional x) (spectralFiniteAverageTest s a w) = ‖∑ i ∈ s, w i • ↑(π (E.inclusion (Multiplicative.ofAdd (a i)))) x‖ ^ 2

theorem Connes.PositiveSpectralFunctional.trivial_atom_le_kernel_orbit_norm_sq {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} [MeasurableSpace (DiscreteCharacterSpace A)] [BorelSpace (DiscreteCharacterSpace A)] {E : SplitAbelianExtension A G H} {V : Type w} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] {π : UnitaryRepresentation G.Carrier V} (Φ : PositiveSpectralFunctional E V π) (x : V) {ι : Type u_1} (s : Finset ι) (a : ι → A) (w : ι → ℝ) (hw : ∑ i ∈ s, w i = 1) : (Φ.measure x).real {1} ≤ ‖∑ i ∈ s, w i • ↑(π (E.inclusion (Multiplicative.ofAdd (a i)))) x‖ ^ 2

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

The HasKernelOrbitAffineApproximation construction used in the Connes rigidity formalization.

Equations

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

theorem Connes.PositiveSpectralFunctional.trivialCharacterProjection_ne_zero_of_atom_pos_of_orbitApproximation {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} [MeasurableSpace (DiscreteCharacterSpace A)] [BorelSpace (DiscreteCharacterSpace A)] {E : SplitAbelianExtension A G H} {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] {π : UnitaryRepresentation G.Carrier V} (Φ : PositiveSpectralFunctional E V π) (approximation : HasKernelOrbitAffineApproximation E π) (x : QuotientFixedUnitVector E V π) (hx : 0 < spectralTrivialAtom (Φ.probabilityMeasure x.vector ⋯)) : (trivialCharacterProjection E π) x.vector ≠ 0

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

noncomputable def Connes.PositiveSpectralFunctional.toSpectralMeasureInterfaceOfOrbitApproximation {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} [MeasurableSpace (DiscreteCharacterSpace A)] [BorelSpace (DiscreteCharacterSpace A)] {E : SplitAbelianExtension A G H} {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] {π : UnitaryRepresentation G.Carrier V} (Φ : PositiveSpectralFunctional E V π) (approximation : HasKernelOrbitAffineApproximation E π) : SpectralMeasureInterface E V π

The toSpectralMeasureInterfaceOfOrbitApproximation construction used in the Connes rigidity formalization.

Equations

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

theorem Connes.spectral_criterion_of_positive_functional_and_orbitApproximation {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} [MeasurableSpace (DiscreteCharacterSpace A)] [BorelSpace (DiscreteCharacterSpace A)] (E : SplitAbelianExtension A G H) (hH : HasKazhdanPropertyT H) (J : Finset A) {c : ℝ} (hc : 0 < c) (hdetection : HasFiniteSpectralDetection E J c) (functional : (V : Type v) → (x : NormedAddCommGroup V) → (x_1 : InnerProductSpace ℂ V) → (x_2 : CompleteSpace V) → (π : UnitaryRepresentation G.Carrier V) → PositiveSpectralFunctional E V π) (approximation : ∀ (V : Type v) (x : NormedAddCommGroup V) (x_1 : InnerProductSpace ℂ V) (x_2 : CompleteSpace V) (π : UnitaryRepresentation G.Carrier V), HasKernelOrbitAffineApproximation E π) : HasKazhdanPropertyT G

def Connes.spectralOperatorGenerators {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier V) : Set (V →L[ℂ] V)

The spectralOperatorGenerators construction used in the Connes rigidity formalization.

Equations

• Connes.spectralOperatorGenerators E π = Set.range fun (a : A) => ↑(π (E.inclusion (Multiplicative.ofAdd a)))

noncomputable def Connes.spectralOperatorAlgebra {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier V) : StarSubalgebra ℂ (V →L[ℂ] V)

The spectralOperatorAlgebra construction used in the Connes rigidity formalization.

Equations

• Connes.spectralOperatorAlgebra E π = (StarAlgebra.adjoin ℂ (Connes.spectralOperatorGenerators E π)).topologicalClosure

theorem Connes.spectralOperatorGenerators_commute {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier V) {S T : V →L[ℂ] V} (hS : S ∈ spectralOperatorGenerators E π) (hT : T ∈ spectralOperatorGenerators E π) : S * T = T * S

theorem Connes.star_mem_spectralOperatorGenerators {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier V) {T : V →L[ℂ] V} (hT : T ∈ spectralOperatorGenerators E π) : star T ∈ spectralOperatorGenerators E π

instance Connes.spectralOperatorAdjoin_isMulCommutative {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier V) : IsMulCommutative ↥(StarAlgebra.adjoin ℂ (spectralOperatorGenerators E π))

@[instance_reducible]

noncomputable instance Connes.spectralOperatorAlgebraCommCStarAlgebra {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier V) : CommCStarAlgebra ↥(spectralOperatorAlgebra E π)

Equations

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

noncomputable def Connes.spectralKernelOperator {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier V) (a : A) : ↥(spectralOperatorAlgebra E π)

The spectralKernelOperator construction used in the Connes rigidity formalization.

Equations

• Connes.spectralKernelOperator E π a = ⟨↑(π (E.inclusion (Multiplicative.ofAdd a))), ⋯⟩

@[simp]

theorem Connes.spectralKernelOperator_coe {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier V) (a : A) : ↑(spectralKernelOperator E π a) = ↑(π (E.inclusion (Multiplicative.ofAdd a)))

@[simp]

theorem Connes.spectralKernelOperator_zero {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier V) : spectralKernelOperator E π 0 = 1

theorem Connes.spectralKernelOperator_add {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier V) (a b : A) : spectralKernelOperator E π (a + b) = spectralKernelOperator E π a * spectralKernelOperator E π b

theorem Connes.spectralKernelOperator_unitary {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier V) (a : A) : spectralKernelOperator E π a ∈ unitary ↥(spectralOperatorAlgebra E π)

theorem Connes.spectralCharacter_generator_mem_circle {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier V) (φ : ↑(WeakDual.characterSpace ℂ ↥(spectralOperatorAlgebra E π))) (a : A) : φ (spectralKernelOperator E π a) ∈ Metric.sphere 0 1

noncomputable def Connes.spectralCharacter {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier V) (φ : ↑(WeakDual.characterSpace ℂ ↥(spectralOperatorAlgebra E π))) : DiscreteCharacterSpace A

The spectralCharacter construction used in the Connes rigidity formalization.

Equations

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

@[simp]

theorem Connes.spectralCharacter_apply_coe {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier V) (φ : ↑(WeakDual.characterSpace ℂ ↥(spectralOperatorAlgebra E π))) (a : A) : ↑((spectralCharacter E π φ) (Multiplicative.ofAdd a)) = φ (spectralKernelOperator E π a)

theorem Connes.spectralCharacter_continuous {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier V) : Continuous (spectralCharacter E π)

noncomputable def Connes.spectralCharacterMap {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier V) : C(↑(WeakDual.characterSpace ℂ ↥(spectralOperatorAlgebra E π)), DiscreteCharacterSpace A)

The spectralCharacterMap construction used in the Connes rigidity formalization.

Equations

• Connes.spectralCharacterMap E π = { toFun := Connes.spectralCharacter E π, continuous_toFun := ⋯ }

noncomputable def Connes.jointFunctionalCalculus {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier V) : C(DiscreteCharacterSpace A, ℂ) →⋆ₐ[ℂ] ↥(spectralOperatorAlgebra E π)

The jointFunctionalCalculus construction used in the Connes rigidity formalization.

Equations

• Connes.jointFunctionalCalculus E π = (gelfandStarTransform ↥(Connes.spectralOperatorAlgebra E π)).symm.toStarAlgHom.comp (ContinuousMap.compStarAlgHom' ℂ ℂ (Connes.spectralCharacterMap E π))

noncomputable def Connes.spectralCharacterEvaluation {A : Type u} [AddCommGroup A] [TopologicalSpace A] (a : A) : C(DiscreteCharacterSpace A, ℂ)

The spectralCharacterEvaluation construction used in the Connes rigidity formalization.

Equations

• Connes.spectralCharacterEvaluation a = { toFun := fun (χ : Connes.DiscreteCharacterSpace A) => ↑(χ (Multiplicative.ofAdd a)), continuous_toFun := ⋯ }

@[simp]

theorem Connes.spectralCharacterEvaluation_apply {A : Type u} [AddCommGroup A] [TopologicalSpace A] (a : A) (χ : DiscreteCharacterSpace A) : (spectralCharacterEvaluation a) χ = ↑(χ (Multiplicative.ofAdd a))

theorem Connes.jointFunctionalCalculus_characterEvaluation {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier V) (a : A) : (jointFunctionalCalculus E π) (spectralCharacterEvaluation a) = spectralKernelOperator E π a

theorem Connes.inverseGelfand_naturality {B : Type u} [CommCStarAlgebra B] {X : Type v} [TopologicalSpace X] (α : B →⋆ₐ[ℂ] B) (p : C(↑(WeakDual.characterSpace ℂ B), X)) (d : C(X, X)) (hp : ∀ (φ : ↑(WeakDual.characterSpace ℂ B)), p ((WeakDual.CharacterSpace.compContinuousMap α) φ) = d (p φ)) (f : C(X, ℂ)) : α ((gelfandStarTransform B).symm (f.comp p)) = (gelfandStarTransform B).symm ((f.comp d).comp p)

noncomputable def Connes.positiveVectorState {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] (x : V) : (V →L[ℂ] V) →L[ℝ] ℝ

The positiveVectorState construction used in the Connes rigidity formalization.

Equations

• Connes.positiveVectorState x = Complex.reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ ((innerSL ℂ) x ∘SL (ContinuousLinearMap.apply ℂ V) x)

theorem Connes.positiveVectorState_star_mul_self {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (x : V) (T : V →L[ℂ] V) : (positiveVectorState x) (star T * T) = ‖T x‖ ^ 2

@[simp]

theorem Connes.positiveVectorState_one {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] (x : V) : (positiveVectorState x) 1 = ‖x‖ ^ 2

theorem Connes.dualCharacterAction_mul {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {H : CountableDiscreteGroup} (action : H.Carrier →* Multiplicative (AddAut A)) (g h : H.Carrier) (χ : DiscreteCharacterSpace A) : dualCharacterAction action (g * h) χ = dualCharacterAction action g (dualCharacterAction action h χ)

@[simp]

theorem Connes.dualCharacterAction_one {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {H : CountableDiscreteGroup} (action : H.Carrier →* Multiplicative (AddAut A)) (χ : DiscreteCharacterSpace A) : dualCharacterAction action 1 χ = χ

noncomputable def Connes.dualCharacterHomeomorph {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {H : CountableDiscreteGroup} (action : H.Carrier →* Multiplicative (AddAut A)) (h : H.Carrier) : DiscreteCharacterSpace A ≃ₜ DiscreteCharacterSpace A

The dualCharacterHomeomorph construction used in the Connes rigidity formalization.

Equations

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

@[simp]

theorem Connes.dualCharacterHomeomorph_apply {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {H : CountableDiscreteGroup} (action : H.Carrier →* Multiplicative (AddAut A)) (h : H.Carrier) (χ : DiscreteCharacterSpace A) : (dualCharacterHomeomorph action h) χ = dualCharacterAction action h χ

def Connes.compactTestPrecomp {X : Type u} [TopologicalSpace X] [CompactSpace X] (e : X ≃ₜ X) (f : CompactlySupportedContinuousMap X ℝ) : CompactlySupportedContinuousMap X ℝ

The compactTestPrecomp construction used in the Connes rigidity formalization.

Equations

• Connes.compactTestPrecomp e f = { toFun := fun (x : X) => f (e x), continuous_toFun := ⋯, hasCompactSupport' := ⋯ }

theorem Connes.rieszMeasure_map_homeomorph {X : Type u} [TopologicalSpace X] [CompactSpace X] [T2Space X] [MeasurableSpace X] [BorelSpace X] (e : X ≃ₜ X) (Λ Λ' : CompactlySupportedContinuousMap X ℝ →ₚ[ℝ] ℝ) (hfunctional : ∀ (f : CompactlySupportedContinuousMap X ℝ), Λ (compactTestPrecomp e f) = Λ' f) : MeasureTheory.Measure.map (⇑e) (RealRMK.rieszMeasure Λ) = RealRMK.rieszMeasure Λ'

theorem Connes.rieszMeasure_dualCharacterAction {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {H : CountableDiscreteGroup} [MeasurableSpace (DiscreteCharacterSpace A)] [BorelSpace (DiscreteCharacterSpace A)] (action : H.Carrier →* Multiplicative (AddAut A)) (h : H.Carrier) (Λ Λ' : CompactlySupportedContinuousMap (DiscreteCharacterSpace A) ℝ →ₚ[ℝ] ℝ) (hfunctional : ∀ (f : CompactlySupportedContinuousMap (DiscreteCharacterSpace A) ℝ), Λ (compactTestPrecomp (dualCharacterHomeomorph action h) f) = Λ' f) : MeasureTheory.Measure.map (dualCharacterAction action h) (RealRMK.rieszMeasure Λ) = RealRMK.rieszMeasure Λ'

theorem Connes.positiveVectorState_unitary_pullback {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (x : V) (U : ↥(unitary (V →L[ℂ] V))) (T : V →L[ℂ] V) : (positiveVectorState x) (star ↑U * T * ↑U) = (positiveVectorState (↑U x)) T

noncomputable def Connes.quotientOperatorConjugation {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier V) (h : H.Carrier) : (V →L[ℂ] V) ≃⋆ₐ[ℂ] V →L[ℂ] V

The quotientOperatorConjugation construction used in the Connes rigidity formalization.

Equations

• Connes.quotientOperatorConjugation E π h = (Unitary.conjStarAlgAut ℂ (V →L[ℂ] V)) (π (E.splitting h))

@[simp]

theorem Connes.quotientOperatorConjugation_apply {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier V) (h : H.Carrier) (T : V →L[ℂ] V) : (quotientOperatorConjugation E π h) T = ↑(π (E.splitting h)) * T * star ↑(π (E.splitting h))

theorem Connes.quotientOperatorConjugation_kernel {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier V) (h : H.Carrier) (a : A) : (quotientOperatorConjugation E π h) ↑(π (E.inclusion (Multiplicative.ofAdd a))) = ↑(π (E.inclusion (Multiplicative.ofAdd ((Multiplicative.toAdd (E.action h)) a))))

theorem Connes.quotientOperatorConjugation_generators_image {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier V) (h : H.Carrier) : ⇑(quotientOperatorConjugation E π h) '' spectralOperatorGenerators E π = spectralOperatorGenerators E π

theorem Connes.quotientOperatorConjugation_mem {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier V) (h : H.Carrier) {T : V →L[ℂ] V} (hT : T ∈ spectralOperatorAlgebra E π) : (quotientOperatorConjugation E π h) T ∈ spectralOperatorAlgebra E π

@[simp]

theorem Connes.quotientOperatorConjugation_inv {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier V) (h : H.Carrier) : quotientOperatorConjugation E π h⁻¹ = (quotientOperatorConjugation E π h).symm

noncomputable def Connes.quotientSpectralOperatorConjugation {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier V) (h : H.Carrier) : ↥(spectralOperatorAlgebra E π) ≃⋆ₐ[ℂ] ↥(spectralOperatorAlgebra E π)

The quotientSpectralOperatorConjugation construction used in the Connes rigidity formalization.

Equations

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

@[simp]

theorem Connes.quotientSpectralOperatorConjugation_coe {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier V) (h : H.Carrier) (T : ↥(spectralOperatorAlgebra E π)) : ↑((quotientSpectralOperatorConjugation E π h) T) = (quotientOperatorConjugation E π h) ↑T

@[simp]

theorem Connes.quotientSpectralOperatorConjugation_kernel {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier V) (h : H.Carrier) (a : A) : (quotientSpectralOperatorConjugation E π h) (spectralKernelOperator E π a) = spectralKernelOperator E π ((Multiplicative.toAdd (E.action h)) a)

theorem Connes.spectralCharacter_quotientConjugation {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier V) (h : H.Carrier) (φ : ↑(WeakDual.characterSpace ℂ ↥(spectralOperatorAlgebra E π))) : spectralCharacter E π ((WeakDual.CharacterSpace.compContinuousMap (quotientSpectralOperatorConjugation E π h).toStarAlgHom) φ) = dualCharacterAction E.action h⁻¹ (spectralCharacter E π φ)

noncomputable def Connes.dualCharacterActionContinuousMap {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {H : CountableDiscreteGroup} (action : H.Carrier →* Multiplicative (AddAut A)) (h : H.Carrier) : C(DiscreteCharacterSpace A, DiscreteCharacterSpace A)

The dualCharacterActionContinuousMap construction used in the Connes rigidity formalization.

Equations

• Connes.dualCharacterActionContinuousMap action h = { toFun := Connes.dualCharacterAction action h, continuous_toFun := ⋯ }

@[simp]

theorem Connes.dualCharacterActionContinuousMap_apply {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {H : CountableDiscreteGroup} (action : H.Carrier →* Multiplicative (AddAut A)) (h : H.Carrier) (χ : DiscreteCharacterSpace A) : (dualCharacterActionContinuousMap action h) χ = dualCharacterAction action h χ

theorem Connes.jointFunctionalCalculus_quotient_covariance {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier V) (h : H.Carrier) (f : C(DiscreteCharacterSpace A, ℂ)) : ↑((jointFunctionalCalculus E π) (f.comp (dualCharacterActionContinuousMap E.action h))) = star ↑(π (E.splitting h)) * ↑((jointFunctionalCalculus E π) f) * ↑(π (E.splitting h))

def Connes.characterRealComplexification {X : Type u} [TopologicalSpace X] (f : CompactlySupportedContinuousMap X ℝ) : C(X, ℂ)

The characterRealComplexification construction used in the Connes rigidity formalization.

Equations

• Connes.characterRealComplexification f = { toFun := fun (y : X) => ↑(f y), continuous_toFun := ⋯ }

@[simp]

theorem Connes.characterRealComplexification_apply {X : Type u} [TopologicalSpace X] (f : CompactlySupportedContinuousMap X ℝ) (y : X) : (characterRealComplexification f) y = ↑(f y)

@[simp]

theorem Connes.characterRealComplexification_add {X : Type u} [TopologicalSpace X] (f g : CompactlySupportedContinuousMap X ℝ) : characterRealComplexification (f + g) = characterRealComplexification f + characterRealComplexification g

@[simp]

theorem Connes.characterRealComplexification_smul {X : Type u} [TopologicalSpace X] (r : ℝ) (f : CompactlySupportedContinuousMap X ℝ) : characterRealComplexification (r • f) = ↑r • characterRealComplexification f

noncomputable def Connes.characterRealSqrt {X : Type u} [TopologicalSpace X] [CompactSpace X] (f : CompactlySupportedContinuousMap X ℝ) : CompactlySupportedContinuousMap X ℝ

The characterRealSqrt construction used in the Connes rigidity formalization.

Equations

• Connes.characterRealSqrt f = { toFun := fun (y : X) => √(f y), continuous_toFun := ⋯, hasCompactSupport' := ⋯ }

@[simp]

theorem Connes.characterRealSqrt_apply {X : Type u} [TopologicalSpace X] [CompactSpace X] (f : CompactlySupportedContinuousMap X ℝ) (y : X) : (characterRealSqrt f) y = √(f y)

theorem Connes.characterRealComplexification_eq_star_mul_sqrt {X : Type u} [TopologicalSpace X] [CompactSpace X] (f : CompactlySupportedContinuousMap X ℝ) (hf : ∀ (y : X), 0 ≤ f y) : characterRealComplexification f = star (characterRealComplexification (characterRealSqrt f)) * characterRealComplexification (characterRealSqrt f)

noncomputable def Connes.characterVectorFunctionalLinear {X : Type u} [TopologicalSpace X] {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (calculus : C(X, ℂ) →⋆ₐ[ℂ] V →L[ℂ] V) (x : V) : CompactlySupportedContinuousMap X ℝ →ₗ[ℝ] ℝ

The characterVectorFunctionalLinear construction used in the Connes rigidity formalization.

Equations

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

@[simp]

theorem Connes.characterVectorFunctionalLinear_apply {X : Type u} [TopologicalSpace X] {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (calculus : C(X, ℂ) →⋆ₐ[ℂ] V →L[ℂ] V) (x : V) (f : CompactlySupportedContinuousMap X ℝ) : (characterVectorFunctionalLinear calculus x) f = (inner ℂ x ((calculus (characterRealComplexification f)) x)).re

theorem Connes.characterVectorFunctionalLinear_nonneg {X : Type u} [TopologicalSpace X] {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] [CompactSpace X] (calculus : C(X, ℂ) →⋆ₐ[ℂ] V →L[ℂ] V) (x : V) (f : CompactlySupportedContinuousMap X ℝ) (hf : ∀ (y : X), 0 ≤ f y) : 0 ≤ (characterVectorFunctionalLinear calculus x) f

noncomputable def Connes.characterVectorFunctional {X : Type u} [TopologicalSpace X] {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] [CompactSpace X] (calculus : C(X, ℂ) →⋆ₐ[ℂ] V →L[ℂ] V) (x : V) : CompactlySupportedContinuousMap X ℝ →ₚ[ℝ] ℝ

The characterVectorFunctional construction used in the Connes rigidity formalization.

Equations

• Connes.characterVectorFunctional calculus x = { toLinearMap := Connes.characterVectorFunctionalLinear calculus x, monotone' := ⋯ }

@[simp]

theorem Connes.characterVectorFunctional_apply {X : Type u} [TopologicalSpace X] {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] [CompactSpace X] (calculus : C(X, ℂ) →⋆ₐ[ℂ] V →L[ℂ] V) (x : V) (f : CompactlySupportedContinuousMap X ℝ) : (characterVectorFunctional calculus x) f = (inner ℂ x ((calculus (characterRealComplexification f)) x)).re

theorem Connes.characterVectorFunctional_one {X : Type u} [TopologicalSpace X] {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] [CompactSpace X] (calculus : C(X, ℂ) →⋆ₐ[ℂ] V →L[ℂ] V) (x : V) (f : CompactlySupportedContinuousMap X ℝ) (hf : ∀ (y : X), f y = 1) : (characterVectorFunctional calculus x) f = ‖x‖ ^ 2

theorem Connes.characterVectorFunctional_energy_of_operator {X : Type u} [TopologicalSpace X] {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] [CompactSpace X] (calculus : C(X, ℂ) →⋆ₐ[ℂ] V →L[ℂ] V) (x : V) (f : CompactlySupportedContinuousMap X ℝ) (T : V →L[ℂ] V) (hf : calculus (characterRealComplexification f) = star (T - 1) * (T - 1)) : (characterVectorFunctional calculus x) f = ‖T x - x‖ ^ 2

theorem Connes.characterEnergy_complexification {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] (a : A) (evaluation : C(DiscreteCharacterSpace A, ℂ)) (hevaluation : ∀ (χ : DiscreteCharacterSpace A), evaluation χ = ↑(χ (Multiplicative.ofAdd a))) : characterRealComplexification (spectralEnergyTest a) = star (evaluation - 1) * (evaluation - 1)

theorem Connes.characterVectorFunctional_spectralEnergy {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] (calculus : C(DiscreteCharacterSpace A, ℂ) →⋆ₐ[ℂ] V →L[ℂ] V) (x : V) (a : A) (evaluation : C(DiscreteCharacterSpace A, ℂ)) (hevaluation : ∀ (χ : DiscreteCharacterSpace A), evaluation χ = ↑(χ (Multiplicative.ofAdd a))) (T : V →L[ℂ] V) (hT : calculus evaluation = T) : (characterVectorFunctional calculus x) (spectralEnergyTest a) = ‖T x - x‖ ^ 2

theorem Connes.characterVectorFunctional_spectralUnit {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] (calculus : C(DiscreteCharacterSpace A, ℂ) →⋆ₐ[ℂ] V →L[ℂ] V) (x : V) : (characterVectorFunctional calculus x) (spectralUnitTest A) = ‖x‖ ^ 2

noncomputable def Connes.jointFunctionalCalculusOperator {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} {W : Type v} [NormedAddCommGroup W] [InnerProductSpace ℂ W] [CompleteSpace W] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier W) : C(DiscreteCharacterSpace A, ℂ) →⋆ₐ[ℂ] W →L[ℂ] W

The jointFunctionalCalculusOperator construction used in the Connes rigidity formalization.

Equations

• Connes.jointFunctionalCalculusOperator E π = (Connes.spectralOperatorAlgebra E π).subtype.comp (Connes.jointFunctionalCalculus E π)

@[simp]

theorem Connes.jointFunctionalCalculusOperator_characterEvaluation {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} {W : Type v} [NormedAddCommGroup W] [InnerProductSpace ℂ W] [CompleteSpace W] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier W) (a : A) : (jointFunctionalCalculusOperator E π) (spectralCharacterEvaluation a) = ↑(π (E.inclusion (Multiplicative.ofAdd a)))

noncomputable def Connes.jointCharacterFunctional {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} {W : Type v} [NormedAddCommGroup W] [InnerProductSpace ℂ W] [CompleteSpace W] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier W) (x : W) : CompactlySupportedContinuousMap (DiscreteCharacterSpace A) ℝ →ₚ[ℝ] ℝ

The jointCharacterFunctional construction used in the Connes rigidity formalization.

Equations

• Connes.jointCharacterFunctional E π x = Connes.characterVectorFunctional (Connes.jointFunctionalCalculusOperator E π) x

@[simp]

theorem Connes.jointCharacterFunctional_apply {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} {W : Type v} [NormedAddCommGroup W] [InnerProductSpace ℂ W] [CompleteSpace W] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier W) (x : W) (f : CompactlySupportedContinuousMap (DiscreteCharacterSpace A) ℝ) : (jointCharacterFunctional E π x) f = (inner ℂ x (((jointFunctionalCalculusOperator E π) (characterRealComplexification f)) x)).re

theorem Connes.jointCharacterFunctional_normalization {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} {W : Type v} [NormedAddCommGroup W] [InnerProductSpace ℂ W] [CompleteSpace W] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier W) (x : W) : (jointCharacterFunctional E π x) (spectralUnitTest A) = ‖x‖ ^ 2

theorem Connes.jointCharacterFunctional_energy {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} {W : Type v} [NormedAddCommGroup W] [InnerProductSpace ℂ W] [CompleteSpace W] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier W) (x : W) (a : A) : (jointCharacterFunctional E π x) (spectralEnergyTest a) = ‖↑(π (E.inclusion (Multiplicative.ofAdd a))) x - x‖ ^ 2

theorem Connes.jointCharacterFunctional_pullback_of_operatorCovariance {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} {W : Type v} [NormedAddCommGroup W] [InnerProductSpace ℂ W] [CompleteSpace W] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier W) (h : H.Carrier) (hcovariance : ∀ (f : C(DiscreteCharacterSpace A, ℂ)), (jointFunctionalCalculusOperator E π) (f.comp { toFun := ⇑(dualCharacterHomeomorph E.action h), continuous_toFun := ⋯ }) = star ↑(π (E.splitting h)) * (jointFunctionalCalculusOperator E π) f * ↑(π (E.splitting h))) (x : W) (f : CompactlySupportedContinuousMap (DiscreteCharacterSpace A) ℝ) : (jointCharacterFunctional E π x) (compactTestPrecomp (dualCharacterHomeomorph E.action h) f) = (jointCharacterFunctional E π (↑(π (E.splitting h)) x)) f

theorem Connes.jointCharacterFunctional_riesz_covariance_of_operatorCovariance {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} {W : Type v} [NormedAddCommGroup W] [InnerProductSpace ℂ W] [CompleteSpace W] [MeasurableSpace (DiscreteCharacterSpace A)] [BorelSpace (DiscreteCharacterSpace A)] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier W) (h : H.Carrier) (hcovariance : ∀ (f : C(DiscreteCharacterSpace A, ℂ)), (jointFunctionalCalculusOperator E π) (f.comp { toFun := ⇑(dualCharacterHomeomorph E.action h), continuous_toFun := ⋯ }) = star ↑(π (E.splitting h)) * (jointFunctionalCalculusOperator E π) f * ↑(π (E.splitting h))) (x : W) : MeasureTheory.Measure.map (dualCharacterAction E.action h) (RealRMK.rieszMeasure (jointCharacterFunctional E π x)) = RealRMK.rieszMeasure (jointCharacterFunctional E π (↑(π (E.splitting h)) x))

def Connes.kernelUnitaryOrbit {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier V) (x : V) : Set V

The kernelUnitaryOrbit construction used in the Connes rigidity formalization.

Equations

• Connes.kernelUnitaryOrbit E π x = Set.range fun (a : A) => ↑(π (E.inclusion (Multiplicative.ofAdd a))) x

def Connes.kernelOrbitClosedConvexHull {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier V) (x : V) : Set V

The kernelOrbitClosedConvexHull construction used in the Connes rigidity formalization.

Equations

• Connes.kernelOrbitClosedConvexHull E π x = (closedConvexHull ℝ) (Connes.kernelUnitaryOrbit E π x)

theorem Connes.mem_kernelOrbitClosedConvexHull {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier V) (x : V) : x ∈ kernelOrbitClosedConvexHull E π x

theorem Connes.kernelUnitary_preserves_closedConvexHull {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier V) (x : V) (a : A) (y : V) : y ∈ kernelOrbitClosedConvexHull E π x → ↑(π (E.inclusion (Multiplicative.ofAdd a))) y ∈ kernelOrbitClosedConvexHull E π x

theorem Connes.exists_kernel_fixed_norm_minimizer {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier V) (x : V) : ∃ y ∈ kernelOrbitClosedConvexHull E π x, (∀ z ∈ kernelOrbitClosedConvexHull E π x, ‖y‖ ≤ ‖z‖) ∧ ∀ (a : A), ↑(π (E.inclusion (Multiplicative.ofAdd a))) y = y

theorem Connes.exists_kernel_fixed_mem_closedConvexHull {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier V) (x : V) : ∃ y ∈ kernelOrbitClosedConvexHull E π x, ∀ (a : A), ↑(π (E.inclusion (Multiplicative.ofAdd a))) y = y

theorem Connes.kernelOrbit_closedConvexHull_projection_eq_zero {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} (E : SplitAbelianExtension A G H) {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (π : UnitaryRepresentation G.Carrier V) (x : V) (hx : (trivialCharacterProjection E π) x = 0) (y : V) : y ∈ (closedConvexHull ℝ) (Set.range fun (a : A) => ↑(π (E.inclusion (Multiplicative.ofAdd a))) x) → (trivialCharacterProjection E π) y = 0

theorem Connes.kernel_fixed_inner_eq_zero_of_mem_closedConvexHull {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} (E : SplitAbelianExtension A G H) {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (π : UnitaryRepresentation G.Carrier V) (x v y : V) (hx : (trivialCharacterProjection E π) x = 0) (hvfixed : ∀ (a : A), ↑(π (E.inclusion (Multiplicative.ofAdd a))) v = v) (hy : y ∈ (closedConvexHull ℝ) (Set.range fun (a : A) => ↑(π (E.inclusion (Multiplicative.ofAdd a))) x)) : inner ℂ v y = 0

theorem Connes.kernel_fixed_eq_zero_of_mem_closedConvexHull {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} (E : SplitAbelianExtension A G H) {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (π : UnitaryRepresentation G.Carrier V) (x v : V) (hx : (trivialCharacterProjection E π) x = 0) (hv : v ∈ (closedConvexHull ℝ) (Set.range fun (a : A) => ↑(π (E.inclusion (Multiplicative.ofAdd a))) x)) (hvfixed : ∀ (a : A), ↑(π (E.inclusion (Multiplicative.ofAdd a))) v = v) : v = 0

theorem Connes.exists_finset_affineCombination_approx_of_mem_closedConvexHull {I : Type u} {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] (orbit : I → V) {y : V} (hy : y ∈ (closedConvexHull ℝ) (Set.range orbit)) {ε : ℝ} (hε : 0 < ε) : ∃ (s : Finset I) (w : I → ℝ), (∀ i ∈ s, 0 ≤ w i) ∧ ∑ i ∈ s, w i = 1 ∧ ‖∑ i ∈ s, w i • orbit i - y‖ < ε

theorem Connes.exists_finset_affineCombination_norm_lt_of_zero_mem_closedConvexHull {I : Type u} {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] (orbit : I → V) (hzero : 0 ∈ (closedConvexHull ℝ) (Set.range orbit)) {ε : ℝ} (hε : 0 < ε) : ∃ (s : Finset I) (w : I → ℝ), (∀ i ∈ s, 0 ≤ w i) ∧ ∑ i ∈ s, w i = 1 ∧ ‖∑ i ∈ s, w i • orbit i‖ < ε

theorem Connes.kernelOrbit_exists_finset_affineCombination_norm_lt {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} (E : SplitAbelianExtension A G H) {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (π : UnitaryRepresentation G.Carrier V) (x : V) (hzero : 0 ∈ (closedConvexHull ℝ) (Set.range fun (a : A) => ↑(π (E.inclusion (Multiplicative.ofAdd a))) x)) {ε : ℝ} (hε : 0 < ε) : ∃ (s : Finset A) (w : A → ℝ), (∀ a ∈ s, 0 ≤ w a) ∧ ∑ a ∈ s, w a = 1 ∧ ‖∑ a ∈ s, w a • ↑(π (E.inclusion (Multiplicative.ofAdd a))) x‖ < ε

theorem Connes.zero_mem_kernelOrbitClosedConvexHull_of_projection_eq_zero {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} (E : SplitAbelianExtension A G H) {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (π : UnitaryRepresentation G.Carrier V) (x : V) (hx : (trivialCharacterProjection E π) x = 0) : 0 ∈ kernelOrbitClosedConvexHull E π x

theorem Connes.kernelOrbitAffineApproximation {A : Type u} [AddCommGroup A] {G H : CountableDiscreteGroup} (E : SplitAbelianExtension A G H) {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (π : UnitaryRepresentation G.Carrier V) : HasKernelOrbitAffineApproximation E π

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

noncomputable def Connes.jointPositiveSpectralFunctional {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} [MeasurableSpace (DiscreteCharacterSpace A)] [BorelSpace (DiscreteCharacterSpace A)] {V : Type v} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V] (E : SplitAbelianExtension A G H) (π : UnitaryRepresentation G.Carrier V) : PositiveSpectralFunctional E V π

The jointPositiveSpectralFunctional construction used in the Connes rigidity formalization.

Equations

• Connes.jointPositiveSpectralFunctional E π = { functional := fun (x : V) => Connes.jointCharacterFunctional E π x, normalization := ⋯, energy := ⋯, covariance := ⋯ }

theorem Connes.spectral_criterion_unconditional {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} [MeasurableSpace (DiscreteCharacterSpace A)] [BorelSpace (DiscreteCharacterSpace A)] (E : SplitAbelianExtension A G H) (hH : HasKazhdanPropertyT H) (J : Finset A) {c : ℝ} (hc : 0 < c) (hdetection : HasFiniteSpectralDetection E J c) : HasKazhdanPropertyT G

Zhou's §4 spectral criterion with no analytic input left as a hypothesis. For a split extension with property-(T) quotient, a positive finite detector on the dual of the abelian kernel implies property-(T) of the total group.