CompactFamilyGeneric.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

A fixed generic set for a compact family of observables

The limiting shear is selected after the generic set. Compactness of the possible shears gives a compact family of translated observables in the uniform norm. A finite approximation therefore suffices for one common generic set and time threshold. No commutation of the translating group with the averaging flow is required.

theorem OAI.DukePrimeDegree.exists_finite_uniform_real_flow_generic_set line 22
lemma OAI.DukePrimeDegree.flow_average_error_of_uniform_approximation line 58

theorem OAI.DukePrimeDegree.exists_compact_family_real_flow_generic_set line 115

Source documentation

Compactness is in the uniform norm on bounded continuous functions.

theorem exists_compact_family_real_flow_generic_set
    {Y : Type*} [TopologicalSpace Y] [MeasurableSpace Y] [BorelSpace Y]
    [MulAction (Multiplicative ℝ) Y] [ContinuousSMul (Multiplicative ℝ) Y]
    (μ : Measure Y) [IsProbabilityMeasure μ] [ErgodicSMul (Multiplicative ℝ) Y μ]
    (K : Set (Y →ᵇ ℝ)) (hK : IsCompact K)
    (ε δ : ℝ) (hε : 0 < ε) (hδ : 0 < δ) :
    ∃ G : Set Y, MeasurableSet G ∧ μ Gᶜ ≤ ENNReal.ofReal δ ∧
      ∃ R : ℝ, 1 ≤ R ∧ ∀ x ∈ G, ∀ f ∈ K, ∀ T ≥ R,
        |T⁻¹ * (∫ t in (0 : ℝ)..T, f (realActionTime t x)) -
          ∫ y, f y ∂μ| ≤ ε := by
…

Mentions: OAI.DukePrimeDegree.realActionTime

def OAI.DukePrimeDegree.compactObservableTranslate line 142
theorem OAI.DukePrimeDegree.continuous_compactObservableTranslate line 148

theorem OAI.DukePrimeDegree.exists_compact_translate_real_flow_generic_set line 167

Source documentation

The translating element may be any later-selected point of a fixed compact set. It is unrelated to the real averaging flow.

theorem exists_compact_translate_real_flow_generic_set
    {H Y : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    [WeaklyLocallyCompactSpace H] [TopologicalSpace Y]
    [MulAction H Y] [ContinuousSMul H Y]
    [MeasurableSpace Y] [BorelSpace Y]
    [MulAction (Multiplicative ℝ) Y] [ContinuousSMul (Multiplicative ℝ) Y]
    (μ : Measure Y) [IsProbabilityMeasure μ] [ErgodicSMul (Multiplicative ℝ) Y μ]
    (f : CompactlySupportedContinuousMap Y ℝ) (K : Set H) (hK : IsCompact K)
    (ε δ : ℝ) (hε : 0 < ε) (hδ : 0 < δ) :
    ∃ G : Set Y, MeasurableSet G ∧ μ Gᶜ ≤ ENNReal.ofReal δ ∧
      ∃ R : ℝ, 1 ≤ R ∧ ∀ x ∈ G, ∀ a ∈ K, ∀ T ≥ R,
        |T⁻¹ * (∫ t in (0 : ℝ)..T, f (a • realActionTime t x)) -
…

Mentions: OAI.DukePrimeDegree.realActionTime