Lax Lean Archive

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

Tempered functions

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

definition

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

    Definition

    Let σ:Ω→Ω\sigma : \Omega \to \Omega be a measurable map and μ\mu a measure on Ω\Omega. A function f:Ω→Rf : \Omega \to \mathbb{R} is tempered if it grows subexponentially along almost every forward orbit:

    lim⁡n→∞f(σnω)n=0for μ-a.e. ω.\lim_{n \to \infty} \frac{f(\sigma^n \omega)}{n} = 0 \quad \text{for } \mu\text{-a.e. } \omega.
    Concept map
    1 concept; 8 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitLab

    1import Mathlib.MeasureTheory.Measure.MeasureSpaceDef
    2
    3/-!
    4---
    5title: Tempered functions
    6type: definition
    7---
    8Let σ:Ω→Ω\sigma : \Omega \to \Omega be a measurable map and μ\mu a measure on Ω\Omega. A function
    9f:Ω→Rf : \Omega \to \mathbb{R} is **tempered** if it grows subexponentially along almost every
    10forward orbit:
    11lim⁡n→∞f(σnω)n=0for μ-a.e. ω.\lim_{n \to \infty} \frac{f(\sigma^n \omega)}{n} = 0 \quad \text{for } \mu\text{-a.e. } \omega.
    12-/
    13
    14namespace Lax606786.TemperedFunctions
    15
    16open MeasureTheory Filter Topology
    17
    18/-- `f(σⁿω)/n → 0` for `μ`-a.e. `ω`. -/
    19def Tempered {Ω : Type*} [MeasurableSpace Ω] (σ : Ω → Ω) (μ : Measure Ω) (f : Ω → ℝ) : Prop :=
    20 ∀ᵐ ω ∂μ, Tendsto (fun n : ℕ => f (σ^[n] ω) / n) atTop (𝓝 0)
    21
    22end Lax606786.TemperedFunctions
    23
    Builds on

    none

    Used by
    From Mathlib

    Discussion

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

    Loading discussion…