Shifting a signature
Lax606786.SignatureShift · concepts/Lax606786/SignatureShift.lean · lax-606786
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
Let , be cocycles and points with for all , where is the index at which the -th distinct exponent of at starts. Then the distinct exponents and multiplicities of at are those of at from the -th on: for every ,
and the starting index of is that of less . If has no -th distinct exponent at , the index at which it would start is the least element of an empty set of natural numbers, which is taken to be ; the conclusion then says that both starting indices are .
Concept map
Evidence
Lean source view on GitLab
| 1 | import Lax606786.Cocycles |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: Shifting a signature |
| 6 | type: theorem |
| 7 | --- |
| 8 | Let , be cocycles and points with |
| 9 | for all , where is the index at which the |
| 10 | -th distinct exponent of at starts. Then the distinct exponents and |
| 11 | multiplicities of at are those of at from the |
| 12 | -th on: for every , |
| 13 | |
| 14 | and the starting index of is that of less . If |
| 15 | has no -th distinct exponent at , the index at which it would start is the least |
| 16 | element of an empty set of natural numbers, which is taken to be ; the conclusion then says |
| 17 | that both starting indices are . |
| 18 | -/ |
| 19 | |
| 20 | namespace Lax606786.SignatureShift |
| 21 | |
| 22 | open Lax606786.Cocycles |
| 23 | |
| 24 | variable {Ω X : Type*} [MeasurableSpace Ω] [StandardBorelSpace Ω] |
| 25 | [NormedAddCommGroup X] [NormedSpace ℝ X] [MeasurableSpace X] |
| 26 | |
| 27 | /-- The exponent indices of a shifted signature are shifted. -/ |
| 28 | axiom 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. -/ |
| 35 | axiom 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 | |
| 40 | end Lax606786.SignatureShift |
| 41 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments