The spectral criterion component of the Connes rigidity formalization.

@[reducible, inline]

abbrev Connes.DiscreteCharacterSpace (A : Type u) [AddCommGroup A] [TopologicalSpace A] : Type u

Pontryagin dual of a discrete additive kernel. Paper: §3--4.

Equations

• Connes.DiscreteCharacterSpace A = PontryaginDual (Multiplicative A)

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

Inverse-dual action of a group on the character space. Paper: §4.

Equations

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

@[simp]

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

theorem Connes.continuous_dualCharacterAction {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {H : CountableDiscreteGroup} (action : H.Carrier →* Multiplicative (AddAut A)) (h : H.Carrier) : Continuous (dualCharacterAction action h)

The inverse-dual action is continuous. Paper: §4.

theorem Connes.measurable_dualCharacterAction {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {H : CountableDiscreteGroup} [MeasurableSpace (PontryaginDual (Multiplicative A))] [BorelSpace (PontryaginDual (Multiplicative A))] (action : H.Carrier →* Multiplicative (AddAut A)) (h : H.Carrier) : Measurable (dualCharacterAction action h)

The inverse-dual action is measurable. Paper: §4.

def Connes.IsInvariantSpectralMeasure {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {H : CountableDiscreteGroup} [MeasurableSpace (PontryaginDual (Multiplicative A))] (action : H.Carrier →* Multiplicative (AddAut A)) (μ : MeasureTheory.ProbabilityMeasure (DiscreteCharacterSpace A)) : Prop

Invariant probability measure for the dual action, whose measurability is recorded by measurable_dualCharacterAction. Paper: §4.

Equations

• Connes.IsInvariantSpectralMeasure action μ = ∀ (h : H.Carrier), MeasureTheory.Measure.map (Connes.dualCharacterAction action h) ↑μ = ↑μ

def Connes.spectralTrivialAtom {A : Type u} [AddCommGroup A] [TopologicalSpace A] [MeasurableSpace (PontryaginDual (Multiplicative A))] (μ : MeasureTheory.ProbabilityMeasure (DiscreteCharacterSpace A)) : ℝ

Mass of the trivial character. Paper: §4.

Equations

• Connes.spectralTrivialAtom μ = (↑μ).real {1}

theorem Connes.continuous_character_evaluation {A : Type u} [AddCommGroup A] [TopologicalSpace A] (a : A) : Continuous fun (χ : DiscreteCharacterSpace A) => ↑(χ (Multiplicative.ofAdd a))

Character evaluation is continuous on the compact dual. Paper: §4.

noncomputable def Connes.spectralEnergyTest {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] (a : A) : CompactlySupportedContinuousMap (DiscreteCharacterSpace A) ℝ

Compactly supported continuous test for spectral displacement. Paper: §4.

Equations

• Connes.spectralEnergyTest a = { toFun := fun (χ : Connes.DiscreteCharacterSpace A) => ‖↑(χ (Multiplicative.ofAdd a)) - 1‖ ^ 2, continuous_toFun := ⋯, hasCompactSupport' := ⋯ }

@[simp]

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

theorem Connes.integrable_spectralEnergyTest {A : Type u} [AddCommGroup A] [TopologicalSpace A] [MeasurableSpace (PontryaginDual (Multiplicative A))] [BorelSpace (PontryaginDual (Multiplicative A))] (μ : MeasureTheory.ProbabilityMeasure (DiscreteCharacterSpace A)) (a : A) : MeasureTheory.Integrable (fun (χ : DiscreteCharacterSpace A) => ‖↑(χ (Multiplicative.ofAdd a)) - 1‖ ^ 2) ↑μ

The spectral displacement integrand is integrable against every probability measure.

noncomputable def Connes.spectralDetectionEnergy {A : Type u} [AddCommGroup A] [TopologicalSpace A] [MeasurableSpace (PontryaginDual (Multiplicative A))] (μ : MeasureTheory.ProbabilityMeasure (DiscreteCharacterSpace A)) (a : A) : ℝ

Spectral displacement energy of a kernel element. Its integrand is integrable by integrable_spectralEnergyTest. Paper: §4.

Equations

• Connes.spectralDetectionEnergy μ a = ∫ (χ : Connes.DiscreteCharacterSpace A), ‖↑(χ (Multiplicative.ofAdd a)) - 1‖ ^ 2 ∂↑μ

structure Connes.QuotientFixedUnitVector {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) : Type v

A normalized vector fixed by the quotient section. Paper: §4.

• vector : K

  The vector component of QuotientFixedUnitVector.

• norm_one : ‖self.vector‖ = 1
• quotient_fixed (h : H.Carrier) : ↑(π (E.splitting h)) self.vector = self.vector

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

Representation-specific spectral input used by the generic criterion. Paper: §4.

• quotient_fixed_approximation : HasKazhdanPropertyT H → π.HasAlmostInvariantUnitVectors → ∀ (J : Finset A) (ε : ℝ), 0 < ε → ∃ (ξ : QuotientFixedUnitVector E K π), ∑ a ∈ J, ‖↑(π (E.inclusion (Multiplicative.ofAdd a))) ξ.vector - ξ.vector‖ ^ 2 < ε
• measure : QuotientFixedUnitVector E K π → MeasureTheory.ProbabilityMeasure (DiscreteCharacterSpace A)

  The measure component of SpectralMeasureInterface.

• measure_invariant (ξ : QuotientFixedUnitVector E K π) : IsInvariantSpectralMeasure E.action (self.measure ξ)
• energy_eq (ξ : QuotientFixedUnitVector E K π) (a : A) : spectralDetectionEnergy (self.measure ξ) a = ‖↑(π (E.inclusion (Multiplicative.ofAdd a))) ξ.vector - ξ.vector‖ ^ 2
• positive_atom_invariant (ξ : QuotientFixedUnitVector E K π) : 0 < spectralTrivialAtom (self.measure ξ) → ∃ (η : K), η ≠ 0 ∧ (∀ (a : A), ↑(π (E.inclusion (Multiplicative.ofAdd a))) η = η) ∧ ∀ (h : H.Carrier), ↑(π (E.splitting h)) η = η

def Connes.HasFiniteSpectralDetection {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} [MeasurableSpace (PontryaginDual (Multiplicative A))] (E : SplitAbelianExtension A G H) (J : Finset A) (c : ℝ) : Prop

Finite spectral detection inequality. Paper: §4.

Equations

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

theorem Connes.exists_positive_spectral_atom {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} [MeasurableSpace (PontryaginDual (Multiplicative A))] (E : SplitAbelianExtension A G H) {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (π : UnitaryRepresentation G.Carrier K) (spectral : SpectralMeasureInterface E K π) (hH : HasKazhdanPropertyT H) (hπ : π.HasAlmostInvariantUnitVectors) (J : Finset A) {c : ℝ} (hc : 0 < c) (hdetection : HasFiniteSpectralDetection E J c) : ∃ (ξ : QuotientFixedUnitVector E K π), 0 < spectralTrivialAtom (spectral.measure ξ)

theorem Connes.spectral_criterion_representation {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] {G H : CountableDiscreteGroup} [MeasurableSpace (PontryaginDual (Multiplicative A))] (E : SplitAbelianExtension A G H) {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (π : UnitaryRepresentation G.Carrier K) (spectral : SpectralMeasureInterface E K π) (hH : HasKazhdanPropertyT H) (J : Finset A) {c : ℝ} (hc : 0 < c) (hdetection : HasFiniteSpectralDetection E J c) (hπ : π.HasAlmostInvariantUnitVectors) : ∃ (ξ : K), ξ ≠ 0 ∧ π.IsInvariant ξ

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