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

Shifting a signature

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

proven

Loading review…

Sign in with ORCID

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}, L′\mathcal{L}' be cocycles and ω,ω′\omega, \omega' points with χk′(ω′)=χM+k(ω)\chi'_k(\omega') = \chi_{M+k}(\omega) for all k≥1k \ge 1, where M+1M + 1 is the index at which the jj-th distinct exponent of L\mathcal{L} at ω\omega starts. Then the distinct exponents and multiplicities of L′\mathcal{L}' at ω′\omega' are those of L\mathcal{L} at ω\omega from the jj-th on: for every i≥0i \ge 0,

    λi+1′(ω′)=λj+i(ω),mi+1′(ω′)=mj+i(ω),\lambda'_{i+1}(\omega') = \lambda_{j+i}(\omega), \qquad m'_{i+1}(\omega') = m_{j+i}(\omega),

    and the starting index of λi+1′\lambda'_{i+1} is that of λj+i\lambda_{j+i} less MM. If L\mathcal{L} has no (j+i)(j+i)-th distinct exponent at ω\omega, the index at which it would start is the least element of an empty set of natural numbers, which is taken to be 00; the conclusion then says that both starting indices are 00.

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

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

    Lean source view on GitLab

    1import Lax606786.Cocycles
    2
    3/-!
    4---
    5title: Shifting a signature
    6type: theorem
    7---
    8Let L\mathcal{L}, L′\mathcal{L}' be cocycles and ω,ω′\omega, \omega' points with
    9χk′(ω′)=χM+k(ω)\chi'_k(\omega') = \chi_{M+k}(\omega) for all k≥1k \ge 1, where M+1M + 1 is the index at which the
    10jj-th distinct exponent of L\mathcal{L} at ω\omega starts. Then the distinct exponents and
    11multiplicities of L′\mathcal{L}' at ω′\omega' are those of L\mathcal{L} at ω\omega from the
    12jj-th on: for every i≥0i \ge 0,
    13λi+1′(ω′)=λj+i(ω),mi+1′(ω′)=mj+i(ω),\lambda'_{i+1}(\omega') = \lambda_{j+i}(\omega), \qquad m'_{i+1}(\omega') = m_{j+i}(\omega),
    14and the starting index of λi+1′\lambda'_{i+1} is that of λj+i\lambda_{j+i} less MM. If L\mathcal{L}
    15has no (j+i)(j+i)-th distinct exponent at ω\omega, the index at which it would start is the least
    16element of an empty set of natural numbers, which is taken to be 00; the conclusion then says
    17that both starting indices are 00.
    18-/
    19
    20namespace Lax606786.SignatureShift
    21
    22open Lax606786.Cocycles
    23
    24variable {Ω X : Type*} [MeasurableSpace Ω] [StandardBorelSpace Ω]
    25 [NormedAddCommGroup X] [NormedSpace ℝ X] [MeasurableSpace X]
    26
    27/-- The exponent indices of a shifted signature are shifted. -/
    28axiom lambdaIdx_shift (R R' : Cocycle Ω X) (ω ω' : Ω) {M j : ℕ}
    29 (hχ : ∀ k : ℕ, 1 ≤ k → R'.chi k ω' = R.chi (M + k) ω)
    30 (hj : R.lambdaIdx j ω = M + 1) (i : ℕ) :
    31 (1 ≤ R'.lambdaIdx (i + 1) ω' ∧ R'.lambdaIdx (i + 1) ω' + M = R.lambdaIdx (j + i) ω) ∨
    32 (R'.lambdaIdx (i + 1) ω' = 0 ∧ R.lambdaIdx (j + i) ω = 0)
    33
    34/-- The exponents and multiplicities of a shifted signature are shifted. -/
    35axiom mult_lambda_shift (R R' : Cocycle Ω X) (ω ω' : Ω) {M j : ℕ}
    36 (hχ : ∀ k : ℕ, 1 ≤ k → R'.chi k ω' = R.chi (M + k) ω)
    37 (hj : R.lambdaIdx j ω = M + 1) (i : ℕ) :
    38 R'.mult (i + 1) ω' = R.mult (j + i) ω ∧ R'.lambda (i + 1) ω' = R.lambda (j + i) ω
    39
    40end Lax606786.SignatureShift
    41
    Show 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…