The spectral detection component of the Connes rigidity formalization.
theorem
Connes.measure_detection_gap_of_uniform_primitive_counts
{α : Type u_1}
{ι : Type u_2}
[MeasurableSpace α]
(μ : MeasureTheory.Measure α)
(primitive : Finset ι)
(detect : ι → Set α)
[DecidableRel fun (x : α) (v : ι) => x ∈ detect v]
(active : Set α)
(e : ι)
(he : e ∈ primitive)
(hdetect : ∀ v ∈ primitive, MeasurableSet (detect v))
(hactive : MeasurableSet active)
(hpointwise : ∀ x ∈ active, primitive.card ≤ 7 * {v ∈ primitive | x ∈ detect v}.card)
(huniform : ∀ v ∈ primitive, μ (detect v) = μ (detect e))
:
theorem
Connes.measureReal_detection_gap_of_uniform_primitive_counts
{α : Type u_1}
{ι : Type u_2}
[MeasurableSpace α]
(μ : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
(primitive : Finset ι)
(detect : ι → Set α)
[DecidableRel fun (x : α) (v : ι) => x ∈ detect v]
(active : Set α)
(e : ι)
(he : e ∈ primitive)
(hdetect : ∀ v ∈ primitive, MeasurableSet (detect v))
(hactive : MeasurableSet active)
(hpointwise : ∀ x ∈ active, primitive.card ≤ 7 * {v ∈ primitive | x ∈ detect v}.card)
(huniform : ∀ v ∈ primitive, μ (detect v) = μ (detect e))
:
theorem
Connes.measureReal_iUnion_le_of_monotone
{α : Type u_1}
[MeasurableSpace α]
(μ : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
(U : ℕ → Set α)
(hmono : Monotone U)
{c : ℝ}
(hbound : ∀ (n : ℕ), μ.real (U n) ≤ c)
:
theorem
Connes.probability_detection_gap_of_exhaustion
{α : Type u_1}
[MeasurableSpace α]
(μ : MeasureTheory.ProbabilityMeasure α)
(zero : α)
(U : ℕ → Set α)
(hzero : MeasurableSet {zero})
(hmono : Monotone U)
(hunion : ⋃ (n : ℕ), U n = {zero}ᶜ)
{p : ℝ}
(hbound : ∀ (n : ℕ), (↑μ).real (U n) ≤ 7 * p)
: