OAI/NumberTheory/DukePrimeDegree/Dynamics/CompactStabilizerSeparation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Finitely many observables separate a compact set from the stabilizer

The eventual shearing contradiction only needs a fixed finite family of generic observables. Continuity and compactness produce that family and a uniform positive separation, directly from the actual measure stabilizer. No empirical-convergence or homogeneous-orbit premise is used.

  1. def OAI.DukePrimeDegree.invarianceDefect line 22
  2. lemma OAI.DukePrimeDegree.continuous_invarianceDefect line 26
  3. lemma OAI.DukePrimeDegree.exists_nonzero_invarianceDefect line 31
  4. theorem OAI.DukePrimeDegree.exists_finite_compact_stabilizer_separators line 45

    Source documentation

    A fixed finite family distinguishes every possible limiting shear in a compact set disjoint from the actual stabilizer.

    theorem exists_finite_compact_stabilizer_separators {n : ℕ}
    (μ : Measure (X n)) [IsFiniteMeasure μ]
    (K : Set (G n)) (hK : IsCompact K)
    (hout : ∀ g ∈ K, g ∉ invariantRightSubgroup μ) :
    ∃ (F : Finset (CompactlySupportedContinuousMap (X n) ℝ)) (ε : ℝ),
      0 < ε ∧ ∀ g ∈ K, ∃ f ∈ F, ε < |invarianceDefect μ f g| := by
…

    Mentions: OAI.DukePrimeDegree.invarianceDefect