Lax Lean Archive

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

Norm bounds for iterates and tempered families

Lax606786.NormGrowthBounds · concepts/Lax606786/NormGrowthBounds.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 L\mathcal{L} be a cocycle on a Banach space XX. Then for all nn, jj and ω\omega

    log⁡+∥Lω(n)∥≤∑i<nlog⁡+∥Lσiω∥,∥Lσ−(n+j)ω(j)∥≤exp⁡∑n<t≤n+jlog⁡+∥Lσ−tω∥,\log^+ \|\mathcal{L}^{(n)}_\omega\| \le \sum_{i < n} \log^+ \|\mathcal{L}_{\sigma^i\omega}\|, \qquad \|\mathcal{L}^{(j)}_{\sigma^{-(n+j)}\omega}\| \le \exp \sum_{n < t \le n + j} \log^+ \|\mathcal{L}_{\sigma^{-t}\omega}\|,

    and if XX is separable with its Borel σ\sigma-algebra, the sums on the left are integrable and log⁡+∥L∥\log^+\|\mathcal{L}\| is tempered along backward orbits: 1nlog⁡+∥Lσ−nω∥→0\frac1n \log^+\|\mathcal{L}_{\sigma^{-n}\omega}\| \to 0 almost everywhere. Finally, if ω↦Pω\omega \mapsto P_\omega is a tempered family of operators, then for almost every ω\omega and every ε>0\varepsilon > 0, ∥Pσnω∥≤eεn\|P_{\sigma^n\omega}\| \le e^{\varepsilon n} for all large nn.

    Concept map
    6 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 ae_tempered_backward proven

    2 eventually_norm_le_of_isTempered proven

    3 integrable_sum_log_norm proven

    4 log_norm_iterate_le proven

    5 norm_iterate_backward_le proven

    Lean source view on GitLab

    1import Lax606786.Cocycles
    2import Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
    3
    4/-!
    5---
    6title: Norm bounds for iterates and tempered families
    7type: theorem
    8---
    9Let L\mathcal{L} be a cocycle on a Banach space XX. Then for all nn, jj and ω\omega
    10log⁡+∥Lω(n)∥≤∑i<nlog⁡+∥Lσiω∥,∥Lσ−(n+j)ω(j)∥≤exp⁡∑n<t≤n+jlog⁡+∥Lσ−tω∥,\log^+ \|\mathcal{L}^{(n)}_\omega\| \le \sum_{i < n} \log^+ \|\mathcal{L}_{\sigma^i\omega}\|, \qquad \|\mathcal{L}^{(j)}_{\sigma^{-(n+j)}\omega}\| \le \exp \sum_{n < t \le n + j} \log^+ \|\mathcal{L}_{\sigma^{-t}\omega}\|,
    11
    12
    13and if XX is separable with its Borel σ\sigma-algebra, the sums on the left are integrable and
    14log⁡+∥L∥\log^+\|\mathcal{L}\| is tempered along backward orbits: 1nlog⁡+∥Lσ−nω∥→0\frac1n \log^+\|\mathcal{L}_{\sigma^{-n}\omega}\| \to 0
    15 almost everywhere. Finally, if ω↦Pω\omega \mapsto P_\omega
    16 is a tempered family of operators, then for almost every ω\omega and every ε>0\varepsilon > 0
    17, ∥Pσnω∥≤eεn\|P_{\sigma^n\omega}\| \le e^{\varepsilon n} for all large nn.
    18-/
    19
    20namespace Lax606786.NormGrowthBounds
    21
    22open MeasureTheory Filter Topology TopologicalSpace
    23open Lax606786.Cocycles
    24
    25variable {Ω X : Type*} [MeasurableSpace Ω] [StandardBorelSpace Ω]
    26 [NormedAddCommGroup X] [NormedSpace ℝ X] [MeasurableSpace X]
    27
    28/-- `log⁺‖𝓛^{(n)}_ω‖ ≤ ∑_{i<n} log⁺‖𝓛_{σⁱω}‖`. -/
    29axiom log_norm_iterate_le (R : Cocycle Ω X) (n : ℕ) (ω : Ω) :
    30 Real.log (max ‖R.iterate n ω‖ 1) ≤
    31 ∑ i ∈ Finset.range n, Real.log (max ‖R.L (R.σ^[i] ω)‖ 1)
    32
    33/-- The backward window bound for norms. -/
    34axiom norm_iterate_backward_le (R : Cocycle Ω X) (ω : Ω) (n j : ℕ) :
    35 ‖R.iterate j ((R.σ.symm : Ω → Ω)^[n + j] ω)‖ ≤ Real.exp (∑ t ∈ Finset.Ioc n (n + j),
    36 Real.log (max ‖R.L ((R.σ.symm : Ω → Ω)^[t] ω)‖ 1))
    37
    38/-- The sums `∑_{i<n} log⁺‖𝓛_{σⁱω}‖` are integrable. -/
    39axiom integrable_sum_log_norm (R : Cocycle Ω X) [SeparableSpace X] [BorelSpace X] (n : ℕ) :
    40 Integrable (fun ω => ∑ i ∈ Finset.range n, Real.log (max ‖R.L (R.σ^[i] ω)‖ 1)) R.μ
    41
    42/-- `log⁺‖𝓛‖` is tempered along backward orbits. -/
    43axiom ae_tempered_backward (R : Cocycle Ω X) [SeparableSpace X] [BorelSpace X] :
    44 ∀ᵐ ω ∂(R.μ), Tendsto (fun n : ℕ =>
    45 Real.log (max ‖R.L ((R.σ.symm : Ω → Ω)^[n] ω)‖ 1) / n) atTop (𝓝 0)
    46
    47/-- A tempered family grows subexponentially along forward orbits. -/
    48axiom eventually_norm_le_of_isTempered (R : Cocycle Ω X) {P : Ω → X →L[ℝ] X}
    49 (h : R.IsTempered P) :
    50 ∀ᵐ ω ∂(R.μ), ∀ ε : ℝ, 0 < ε → ∀ᶠ n : ℕ in atTop, ‖P (R.σ^[n] ω)‖ ≤ Real.exp (n * ε)
    51
    52end Lax606786.NormGrowthBounds
    53
    Show ProofShow ProofShow ProofShow 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…