FiniteActionAverage.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Averaging over the finite cycle action

These are the finite-sum projection identities used in the tree cycle reduction. The action will be reciprocal multiplication on cycle leaves.

def OAI.Ostmann.actionPermutation line 17
def OAI.Ostmann.finiteActionAverage line 23
theorem OAI.Ostmann.finiteActionAverage_invariant line 27
theorem OAI.Ostmann.finiteActionAverage_of_invariant line 35
theorem OAI.Ostmann.finiteActionAverage_idempotent line 42

theorem OAI.Ostmann.finiteActionAverage_correlation line 48

Source documentation

Averaging does not change correlation against an action-invariant test.

theorem finiteActionAverage_correlation {G Ω : Type*} [Group G] [Fintype G]
    [Fintype Ω] [MulAction G Ω] (f h : Ω → ℂ)
    (hh : ∀ (g : G) x, h (g • x) = h x) :
    (∑ x : Ω, finiteActionAverage (G := G) f x * conj (h x)) =
…

Mentions: OAI.Ostmann.finiteActionAverage

theorem OAI.Ostmann.finiteActionAverage_norm_sq_le line 65
Source documentation
Jensen's inequality for the finite average, written as a counting sum.
```
theorem finiteActionAverage_norm_sq_le {G Ω : Type*} [Group G] [Fintype G] [MulAction G Ω]
    (f : Ω → ℂ) (x : Ω) :
    ‖finiteActionAverage (G := G) f x‖ ^ 2 ≤
…
```
Mentions: OAI.Ostmann.finiteActionAverage

theorem OAI.Ostmann.finiteActionAverage_energy_le line 83

Source documentation

The cycle average is an L² contraction.

theorem finiteActionAverage_energy_le {G Ω : Type*} [Group G] [Fintype G]
    [Fintype Ω] [MulAction G Ω] (f : Ω → ℂ) :
    (∑ x : Ω, ‖finiteActionAverage (G := G) f x‖ ^ 2) ≤ ∑ x : Ω, ‖f x‖ ^ 2 := by
…

Mentions: OAI.Ostmann.finiteActionAverage