Lax Lean Archive

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

Subadditive families of measurable functions

Lax606786.SubadditiveFamilies · concepts/Lax606786/SubadditiveFamilies.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 map on a measurable space. A sequence (fn)n≥0(f_n)_{n \ge 0} of measurable functions Ω→R\Omega \to \mathbb{R} is a subadditive family over σ\sigma if

    fm+n(ω)≤fm(σnω)+fn(ω)for all m,n≥0 and ω∈Ω.f_{m+n}(\omega) \le f_m(\sigma^n \omega) + f_n(\omega) \quad \text{for all } m, n \ge 0 \text{ and } \omega \in \Omega.

    The typical example is fn(ω)=log⁡∥Lω(n)∥f_n(\omega) = \log \|\mathcal{L}^{(n)}_\omega\| for a cocycle L\mathcal{L} of bounded operators.

    Concept map
    1 concept; 2 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    In the paper

    • page 6 of this submission's paper

    Lean source view on GitLab

    1import Mathlib.MeasureTheory.Constructions.BorelSpace.Real
    2
    3/-!
    4---
    5title: Subadditive families of measurable functions
    6type: definition
    7---
    8Let σ:Ω→Ω\sigma : \Omega \to \Omega be a map on a measurable space. A sequence
    9(fn)n≥0(f_n)_{n \ge 0} of measurable functions Ω→R\Omega \to \mathbb{R} is a **subadditive family**
    10over σ\sigma if
    11fm+n(ω)≤fm(σnω)+fn(ω)for all m,n≥0 and ω∈Ω.f_{m+n}(\omega) \le f_m(\sigma^n \omega) + f_n(\omega) \quad \text{for all } m, n \ge 0 \text{ and } \omega \in \Omega.
    12
    13The typical example is fn(ω)=log⁡∥Lω(n)∥f_n(\omega) = \log \|\mathcal{L}^{(n)}_\omega\| for a cocycle
    14L\mathcal{L} of bounded operators.
    15-/
    16
    17namespace Lax606786.SubadditiveFamilies
    18
    19/-- `(f_n)` is a subadditive family of measurable functions over `σ`. -/
    20def IsSubadditiveFamily {Ω : Type*} [MeasurableSpace Ω] (σ : Ω → Ω) (f : ℕ → Ω → ℝ) : Prop :=
    21 (∀ n, Measurable (f n)) ∧ ∀ m n ω, f (m + n) ω ≤ f m (σ^[n] ω) + f n ω
    22
    23end Lax606786.SubadditiveFamilies
    24
    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…