Lax Lean Archive

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

Linear combinations of weakly subadditive families

Lax606786.WeaklySubadditiveCombinations · concepts/Lax606786/WeaklySubadditiveCombinations.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 invertible ergodic measure-preserving transformation of a nonatomic standard probability space (Ω,μ)(\Omega, \mu). Let fn,gn:Ω→Rf_n, g_n : \Omega \to \mathbb{R} be measurable and weakly subadditive: for constants Kf,KgK_f, K_g and all m,n,ωm, n, \omega,

    fm+n(ω)≤fm(σnω)+fn(ω)+Kf,gm+n(ω)≤gm(σnω)+gn(ω)+Kg,f_{m+n}(\omega) \le f_m(\sigma^n\omega) + f_n(\omega) + K_f, \qquad g_{m+n}(\omega) \le g_m(\sigma^n\omega) + g_n(\omega) + K_g,

    with f1+,g1+f_1^+, g_1^+ integrable. Suppose fn/n→Cff_n/n \to C_f and gn/n→Cgg_n/n \to C_g almost everywhere, with Cf,Cg∈[−∞,∞)C_f, C_g \in [-\infty, \infty), and let t∈Rt \in \mathbb{R}, with t≥0t \ge 0 if Cf=Cg=−∞C_f = C_g = -\infty. Then hn=fn+tgnh_n = f_n + t g_n satisfies, almost everywhere,

    hn(ω)n,hn(σnω)n,h2n(σ−nω)2n ⟶ Cf+t Cg,\frac{h_n(\omega)}{n},\quad \frac{h_n(\sigma^n\omega)}{n},\quad \frac{h_{2n}(\sigma^{-n}\omega)}{2n}\ \longrightarrow\ C_f + t\, C_g,

    where t⋅(−∞)t \cdot (-\infty) is −∞-\infty, 00 or +∞+\infty according as t>0t > 0, t=0t = 0 or t<0t < 0. This is Lemma 25 of Lee (2024).

    Concept map
    1 concept
    100%
    Proven claimThis concept
    Evidence

    Each proof establishes this claim relative to its assumptions.

    In the paper

    • page 9 of this submission's paper

    Lean source view on GitLab

    1import Mathlib.Dynamics.Ergodic.Ergodic
    2import Mathlib.MeasureTheory.Function.L1Space.Integrable
    3import Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass
    4import Mathlib.MeasureTheory.Constructions.Polish.Basic
    5import Mathlib.Data.EReal.Operations
    6
    7/-!
    8---
    9title: Linear combinations of weakly subadditive families
    10type: theorem
    11---
    12Let σ\sigma be an invertible ergodic measure-preserving transformation of a nonatomic standard
    13probability space (Ω,μ)(\Omega, \mu). Let fn,gn:Ω→Rf_n, g_n : \Omega \to \mathbb{R} be measurable and *weakly
    14subadditive*: for constants Kf,KgK_f, K_g and all m,n,ωm, n, \omega,
    15fm+n(ω)≤fm(σnω)+fn(ω)+Kf,gm+n(ω)≤gm(σnω)+gn(ω)+Kg,f_{m+n}(\omega) \le f_m(\sigma^n\omega) + f_n(\omega) + K_f, \qquad g_{m+n}(\omega) \le g_m(\sigma^n\omega) + g_n(\omega) + K_g,
    16
    17with f1+,g1+f_1^+, g_1^+ integrable. Suppose fn/n→Cff_n/n \to C_f and gn/n→Cgg_n/n \to C_g almost everywhere,
    18with Cf,Cg∈[−∞,∞)C_f, C_g \in [-\infty, \infty), and let t∈Rt \in \mathbb{R}, with t≥0t \ge 0 if
    19Cf=Cg=−∞C_f = C_g = -\infty. Then hn=fn+tgnh_n = f_n + t g_n satisfies, almost everywhere,
    20hn(ω)n,hn(σnω)n,h2n(σ−nω)2n ⟶ Cf+t Cg,\frac{h_n(\omega)}{n},\quad \frac{h_n(\sigma^n\omega)}{n},\quad \frac{h_{2n}(\sigma^{-n}\omega)}{2n}\ \longrightarrow\ C_f + t\, C_g,
    21
    22where t⋅(−∞)t \cdot (-\infty) is −∞-\infty, 00 or +∞+\infty according as t>0t > 0, t=0t = 0 or
    23t<0t < 0. This is Lemma 25 of Lee (2024).
    24-/
    25
    26namespace Lax606786.WeaklySubadditiveCombinations
    27
    28open MeasureTheory Filter Topology
    29
    30/-- The forward, shifted and balanced averages of `f + t g` converge to `C_f + t C_g`. -/
    31axiom tendsto_add_smul {Ω : Type*} [MeasurableSpace Ω] [StandardBorelSpace Ω]
    32 (μ : Measure Ω) [IsProbabilityMeasure μ] [NullSingletonClass μ]
    33 (σ : Ω ≃ᵐ Ω) (hσ : Ergodic σ μ)
    34 (f g : ℕ → Ω → ℝ) (Kf Kg : ℝ)
    35 (hf : (∀ n, Measurable (f n)) ∧ ∀ m n ω, f (m + n) ω ≤ f m (σ^[n] ω) + f n ω + Kf)
    36 (hg : (∀ n, Measurable (g n)) ∧ ∀ m n ω, g (m + n) ω ≤ g m (σ^[n] ω) + g n ω + Kg)
    37 (hf1 : Integrable (fun ω => max (f 1 ω) 0) μ)
    38 (hg1 : Integrable (fun ω => max (g 1 ω) 0) μ)
    39 (t : ℝ) (Cf Cg : EReal) (hCf : Cf ≠ ⊤) (hCg : Cg ≠ ⊤)
    40 (hdef : Cf = ⊥ → Cg = ⊥ → 0 ≤ t)
    41 (hCfl : ∀ᵐ ω ∂μ, Tendsto (fun n : ℕ => (f n ω / n : EReal)) atTop (𝓝 Cf))
    42 (hCgl : ∀ᵐ ω ∂μ, Tendsto (fun n : ℕ => (g n ω / n : EReal)) atTop (𝓝 Cg)) :
    43 ∀ᵐ ω ∂μ,
    44 Tendsto (fun n : ℕ => ((f n ω + t * g n ω) / n : EReal)) atTop
    45 (𝓝 (Cf + (t : EReal) * Cg)) ∧
    46 Tendsto (fun n : ℕ => ((f n (σ^[n] ω) + t * g n (σ^[n] ω)) / n : EReal)) atTop
    47 (𝓝 (Cf + (t : EReal) * Cg)) ∧
    48 Tendsto (fun n : ℕ =>
    49 ((f (2 * n) ((σ.symm : Ω → Ω)^[n] ω) + t * g (2 * n) ((σ.symm : Ω → Ω)^[n] ω)) /
    50 (2 * n) : EReal))
    51 atTop (𝓝 (Cf + (t : EReal) * Cg))
    52
    53end Lax606786.WeaklySubadditiveCombinations
    54
    Show Proof
    Builds on

    none

    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…