RightObservableUniformity.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform observables near a compact family of right translations

The tolerance is selected before the eventual shearing limit. Matrix entry control then bounds a compact observable at every base point, including points outside compact subsets of the lattice space.

def OAI.DukePrimeDegree.rightCompactObservable line 21
lemma OAI.DukePrimeDegree.continuous_rightCompactObservable line 40

theorem OAI.DukePrimeDegree.exists_uniform_right_observable_tolerance line 49

Source documentation

A single matrix tolerance works around the whole compact set and for every lattice base point.

theorem exists_uniform_right_observable_tolerance {n : ℕ}
    (f : CompactlySupportedContinuousMap (X n) ℝ)
    (K : Set (G n)) (hK : IsCompact K) (ε : ℝ) (hε : 0 < ε) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ g h : G n, h ∈ K → slMatrixDifference g h < δ →
      ∀ x : X n, |f (rightAction x g) - f (rightAction x h)| < ε := by
…

Mentions: OAI.DukePrimeDegree.slMatrixDifference

theorem OAI.DukePrimeDegree.exists_finite_uniform_right_observable_tolerance line 80

Source documentation

Finitely many separating tests share one tolerance, with no choice of a limiting shear involved.

theorem exists_finite_uniform_right_observable_tolerance {n : ℕ}
    (F : Finset (CompactlySupportedContinuousMap (X n) ℝ))
    (K : Set (G n)) (hK : IsCompact K) (ε : ℝ) (hε : 0 < ε) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ f ∈ F, ∀ g h : G n, h ∈ K →
      slMatrixDifference g h < δ →
        ∀ x : X n, |f (rightAction x g) - f (rightAction x h)| < ε := by
…

Mentions: OAI.DukePrimeDegree.slMatrixDifference