Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Criteria for temperedness

Lax606786.TemperedCriteria · concepts/Lax606786/TemperedCriteria.lean · lax-606786

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    Let σ\sigma be an ergodic measure-preserving transformation of a probability space (Ω,μ)(\Omega, \mu).

    • Every measurable integrable g:Ω→Rg : \Omega \to \mathbb{R} is tempered: g(σnω)/n→0g(\sigma^n\omega)/n \to 0 almost everywhere.
    • (Mañé's lemma.) Let g≥0g \ge 0 and hh be measurable, with hh integrable, and suppose g≤h+g∘σg \le h + g \circ \sigma almost everywhere. Then gg is tempered.

    Mañé's lemma is from Mañé (1983); see also González-Tokman and Quas (2015, Lemma 15).

    Concept map
    2 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 2 statements. Each proof establishes one of them relative to its assumptions.

    1 tempered_of_integrable proven

    2 tempered_of_le_add_comp proven

    Lean source view on GitLab

    1import Lax606786.TemperedFunctions
    2import Mathlib.Dynamics.Ergodic.Ergodic
    3import Mathlib.MeasureTheory.Function.L1Space.Integrable
    4
    5/-!
    6---
    7title: Criteria for temperedness
    8type: theorem
    9---
    10Let σ\sigma be an ergodic measure-preserving transformation of a probability space
    11(Ω,μ)(\Omega, \mu).
    12
    13- Every measurable integrable g:Ω→Rg : \Omega \to \mathbb{R} is tempered: g(σnω)/n→0g(\sigma^n\omega)/n \to 0
    14 almost everywhere.
    15- (Mañé's lemma.) Let g≥0g \ge 0 and hh be measurable, with hh integrable, and suppose
    16 g≤h+g∘σg \le h + g \circ \sigma almost everywhere. Then gg is tempered.
    17
    18Mañé's lemma is from Mañé (1983); see also González-Tokman and Quas (2015, Lemma 15).
    19-/
    20
    21namespace Lax606786.TemperedCriteria
    22
    23open MeasureTheory
    24open Lax606786.TemperedFunctions
    25
    26variable {Ω : Type*} [MeasurableSpace Ω]
    27
    28/-- Integrable functions are tempered. -/
    29axiom tempered_of_integrable (μ : Measure Ω) [IsProbabilityMeasure μ] (σ : Ω → Ω)
    30 (hσ : Ergodic σ μ) (g : Ω → ℝ) (hg : Measurable g) (hint : Integrable g μ) :
    31 Tempered σ μ g
    32
    33/-- Mañé's lemma: a nonnegative function that can drop by at most an integrable amount along
    34each step of the orbit is tempered. -/
    35axiom tempered_of_le_add_comp (μ : Measure Ω) [IsProbabilityMeasure μ] (σ : Ω → Ω)
    36 (hσ : Ergodic σ μ) (g h : Ω → ℝ) (hg : Measurable g) (hg0 : ∀ ω, 0 ≤ g ω)
    37 (hh : Measurable h) (hint : Integrable h μ) (hle : ∀ᵐ ω ∂μ, g ω ≤ h ω + g (σ ω)) :
    38 Tempered σ μ g
    39
    40end Lax606786.TemperedCriteria
    41
    Show ProofShow Proof
    Builds on
    Used by

    none

    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…