ApproximateInvariantMean.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Constructing an invariant mean from approximate finite averages

Compactness is applied to the actual bounded-function space. The conclusion is the invariant mean used by the height-correction argument, not a separate amenability predicate.

theorem OAI.PolycyclicRecognition.positive_normalized_bound line 26

Source documentation

Positivity and normalization control every bounded real function.

theorem positive_normalized_bound
    (L : BoundedReal G →ₗ[ℝ] ℝ)
    (hpos : ∀ f, (∀ g, 0 ≤ f g) → 0 ≤ L f) (hone : L 1 = 1)
    (f : BoundedReal G) : |L f| ≤ ‖f‖ := by
…

theorem OAI.PolycyclicRecognition.exists_partially_invariantMean_of_approximate line 47

Source documentation

Compactness simultaneously preserves positivity, normalization and vanishing translation defects for any prescribed set of group elements.

theorem exists_partially_invariantMean_of_approximate
    {ι : Type*} {l : Filter ι} [l.NeBot]
    (L : ι → BoundedReal G →ₗ[ℝ] ℝ)
    (hpos : ∀ i f, (∀ g, 0 ≤ f g) → 0 ≤ L i f)
    (hone : ∀ i, L i 1 = 1)
    (S : Set G)
    (hdefect : ∀ g ∈ S, ∀ f, Tendsto (fun i => L i (leftPull g f) - L i f) l (𝓝 0)) :
    ∃ M : BoundedReal G →ₗ[ℝ] ℝ,
      (∀ f, (∀ g, 0 ≤ f g) → 0 ≤ M f) ∧ M 1 = 1 ∧
        ∀ g ∈ S, ∀ f, M (leftPull g f) = M f := by
…

theorem OAI.PolycyclicRecognition.exists_invariantMean_of_approximate line 92

Source documentation

A nontrivial net of positive normalized linear averages whose translation defects tend to zero yields the actual invariant mean used for height correction.

theorem exists_invariantMean_of_approximate
    {ι : Type*} {l : Filter ι} [l.NeBot]
    (L : ι → BoundedReal G →ₗ[ℝ] ℝ)
    (hpos : ∀ i f, (∀ g, 0 ≤ f g) → 0 ≤ L i f)
    (hone : ∀ i, L i 1 = 1)
    (hdefect : ∀ g f, Tendsto (fun i => L i (leftPull g f) - L i f) l (𝓝 0)) :
    Nonempty (InvariantMean G) := by
…