DenseActionAverages.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Jointly ergodic averaging for a continuous group action

The averaged Koopman operator uses a finite topologically generating family. Its common fixed vectors are constant by group ergodicity and continuity of the L2 action. No generator is assumed ergodic.

def OAI.DukePrimeDegree.actionKoopman line 30
lemma OAI.DukePrimeDegree.actionKoopman_apply line 35
lemma OAI.DukePrimeDegree.actionKoopman_norm line 39
theorem OAI.DukePrimeDegree.finite_action_average_fixed_constant line 45
Source documentation
The fixed space of the finite averaging operator consists of constants, using ergodicity of the entire acting group.
```
theorem finite_action_average_fixed_constant
    (a : I → Gᵈᵐᵃ)
    (hdense : Dense (Subgroup.closure (range a) : Set Gᵈᵐᵃ))
    (f : Lp ℝ 2 μ)
    (hfix : finiteIsometryAverage (actionKoopman μ ∘ a) f = f) :
    ∃ c : ℝ, f = constantL2 μ c := by
…
```
Mentions: OAI.DukePrimeDegree.finiteIsometryAverage, OAI.DukePrimeDegree.actionKoopman, OAI.DukePrimeDegree.constantL2
theorem OAI.DukePrimeDegree.finite_action_average_tendsto_constant line 64
lemma OAI.DukePrimeDegree.meanL2_actionKoopman line 88
lemma OAI.DukePrimeDegree.meanL2_finite_action_average line 94
lemma OAI.DukePrimeDegree.meanL2_finite_action_iterate line 105
lemma OAI.DukePrimeDegree.meanL2_finite_action_birkhoff line 113
theorem OAI.DukePrimeDegree.finite_action_average_tendsto_integral line 125
Source documentation
Joint ergodicity gives convergence to the integral without assuming ergodicity of any single member of the finite generating family.
```
theorem finite_action_average_tendsto_integral
    (a : I → Gᵈᵐᵃ)
    (hdense : Dense (Subgroup.closure (range a) : Set Gᵈᵐᵃ))
    (f : Lp ℝ 2 μ) :
    Tendsto
      (fun N => birkhoffAverage ℝ (finiteIsometryAverage (actionKoopman μ ∘ a)) id N f)
      atTop (𝓝 (constantL2 μ (∫ x, f x ∂μ))) := by
…
```
Mentions: OAI.DukePrimeDegree.finiteIsometryAverage, OAI.DukePrimeDegree.actionKoopman, OAI.DukePrimeDegree.constantL2
theorem OAI.DukePrimeDegree.diagonal_action_average_tendsto_integral line 160
Source documentation
The concrete one-and-square-root-of-two coordinate generators give the full diagonal-action average, assuming only A-ergodicity.
```
theorem diagonal_action_average_tendsto_integral (f : Lp ℝ 2 μ) :
    Tendsto (fun N => birkhoffAverage ℝ
      (finiteIsometryAverage (actionKoopman μ ∘ domainParameterGenerators (I := J))) id N f)
…
```
Mentions: OAI.DukePrimeDegree.finiteIsometryAverage, OAI.DukePrimeDegree.actionKoopman, OAI.DukePrimeDegree.domainParameterGenerators
theorem OAI.DukePrimeDegree.dominated_diagonal_action_average_tendsto_integral line 169
Source documentation
The same concrete group averages converge under moving laws with a uniform density bound. None of the individual diagonal translations needs to be ergodic.
```
theorem dominated_diagonal_action_average_tendsto_integral (f : Lp ℝ 2 μ)
    (ν : ℕ → Measure X) [∀ n, IsProbabilityMeasure (ν n)]
    (C : ℝ) (hC : 0 ≤ C) (hdom : ∀ n, ν n ≤ ENNReal.ofReal C • μ) :
    Tendsto (fun N => ∫ x,
      (birkhoffAverage ℝ
        (finiteIsometryAverage (actionKoopman μ ∘ domainParameterGenerators (I := J))) id N f) x
…
```
Mentions: OAI.DukePrimeDegree.finiteIsometryAverage, OAI.DukePrimeDegree.actionKoopman, OAI.DukePrimeDegree.domainParameterGenerators