Lax Lean Archive

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

Sums and bounds of tempered functions

Lax606786.TemperedFunctionAlgebra · concepts/Lax606786/TemperedFunctionAlgebra.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 : \Omega \to \Omega be measurable and μ\mu a measure. The zero function is tempered; sums of tempered functions, and constants added to them, are tempered; a nonnegative function bounded by a tempered one is tempered. If ff is tempered then for almost every ω\omega and every ε>0\varepsilon > 0, f(σnω)≤εnf(\sigma^n\omega) \le \varepsilon n for all large nn.

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

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

    1 eventually_le proven

    2 tempered_add proven

    3 tempered_const_add proven

    4 tempered_of_le proven

    5 tempered_zero proven

    Lean source view on GitLab

    1import Lax606786.TemperedFunctions
    2
    3/-!
    4---
    5title: Sums and bounds of tempered functions
    6type: theorem
    7---
    8Let σ:Ω→Ω\sigma : \Omega \to \Omega be measurable and μ\mu a measure. The zero function is tempered;
    9sums of tempered functions, and constants added to them, are tempered; a nonnegative function
    10bounded by a tempered one is tempered. If ff is tempered then for almost every ω\omega and every
    11ε>0\varepsilon > 0, f(σnω)≤εnf(\sigma^n\omega) \le \varepsilon n for all large nn.
    12-/
    13
    14namespace Lax606786.TemperedFunctionAlgebra
    15
    16open MeasureTheory Filter
    17open Lax606786.TemperedFunctions
    18
    19variable {Ω : Type*} [MeasurableSpace Ω]
    20
    21/-- `0` is tempered. -/
    22axiom tempered_zero {σ : Ω → Ω} {μ : Measure Ω} : Tempered σ μ (fun _ => (0 : ℝ))
    23
    24/-- Sums of tempered functions are tempered. -/
    25axiom tempered_add {σ : Ω → Ω} {μ : Measure Ω} {f g : Ω → ℝ}
    26 (hf : Tempered σ μ f) (hg : Tempered σ μ g) : Tempered σ μ (fun ω => f ω + g ω)
    27
    28/-- Adding a constant preserves temperedness. -/
    29axiom tempered_const_add {σ : Ω → Ω} {μ : Measure Ω} {g : Ω → ℝ} (c : ℝ)
    30 (hg : Tempered σ μ g) : Tempered σ μ (fun ω => c + g ω)
    31
    32/-- A nonnegative function bounded by a tempered one is tempered. -/
    33axiom tempered_of_le {σ : Ω → Ω} {μ : Measure Ω} {f g : Ω → ℝ}
    34 (hg : Tempered σ μ g) (h0 : ∀ ω, 0 ≤ f ω) (hle : ∀ ω, f ω ≤ g ω) : Tempered σ μ f
    35
    36/-- A tempered function is eventually below `ε n` along almost every orbit. -/
    37axiom eventually_le {σ : Ω → Ω} {μ : Measure Ω} {f : Ω → ℝ}
    38 (hf : Tempered σ μ f) : ∀ᵐ ω ∂μ, ∀ ε > 0, ∀ᶠ n : ℕ in atTop, f (σ^[n] ω) ≤ ε * n
    39
    40end Lax606786.TemperedFunctionAlgebra
    41
    Show ProofShow ProofShow ProofShow ProofShow Proof
    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

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

    Loading discussion…