FiniteKoopmanAverages.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Finite averages of Koopman operators

An average of finitely many Hilbert-space isometries has exactly their common fixed vectors. This permits averaging an entire generating family of an ergodic action without asserting that one chosen group element is ergodic.

lemma OAI.DukePrimeDegree.eq_of_equal_norms_and_barycenter line 28
def OAI.DukePrimeDegree.finiteIsometryAverage line 52
lemma OAI.DukePrimeDegree.finiteIsometryAverage_apply line 56
theorem OAI.DukePrimeDegree.finiteIsometryAverage_fixed_iff line 60
theorem OAI.DukePrimeDegree.finiteIsometryAverage_norm_le line 76
theorem OAI.DukePrimeDegree.fixed_of_dense_generators line 101
Source documentation
Continuity extends fixedness under a finite or infinite generating family to fixedness under the full group when its algebraic closure is dense. This will be applied to the continuous L2 domain action.
```
theorem fixed_of_dense_generators (a : I → G)
    (hdense : Dense (Subgroup.closure (range a) : Set G))
    (v : Y) (hfix : ∀ i, a i • v = v) : ∀ g : G, g • v = v := by
…
```

theorem OAI.DukePrimeDegree.ae_eq_const_of_group_invariant line 123

Source documentation

Group ergodicity supplies constant invariant observables directly; no selected element is assumed ergodic.

theorem ae_eq_const_of_group_invariant (f : X → ℝ)
    (hf : AEStronglyMeasurable f μ)
    (hinv : ∀ g : G, (fun x => f (g • x)) =ᵐ[μ] f) :
    ∃ c : ℝ, f =ᵐ[μ] fun _ => c := by
…