CartanPivotCoordinateBound.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The source pivot leaves only a subexponential coordinate loss

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_pivot_cancelled_coordinate_bound line 20

Source documentation

Scalar dilation cancels before estimating the residual action.

theorem exists_pivot_cancelled_coordinate_bound (β : M.Bases) :
    ∃ (A : ℝ) (p : ℕ), 0 ≤ A ∧ ∀ (h : H) (v : cartanRootIdeal H),
      ‖(WordBasisSelections.basis M.letter M.wordList β).equivFun
        (cartanIdealAdjointAutomorphism T H (-h) (cartanIdealWeightDilation T H h v))‖ ≤
      A * (1 + ‖(finBasis ℝ H).equivFun h‖) ^ p *
        ‖(WordBasisSelections.basis M.letter M.wordList β).equivFun v‖ := by
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.WordBasisSelections.basis, OAI.PolycyclicRecognition.cartanIdealAdjointAutomorphism, OAI.PolycyclicRecognition.cartanIdealWeightDilation

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_sequence_pivot_coordinate_bound line 34

Source documentation

Every family of bounded pivot logarithms has one subexponential loss, uniform in the small exponential rate of the bridge input.

theorem exists_sequence_pivot_coordinate_bound (β : M.Bases)
    (scale RH R : ℕ → ℝ) (hs : Tendsto scale atTop atTop)
    (hRH0 : ∀ n, 0 ≤ RH n) (hR0 : ∀ n, 0 ≤ R n)
    (hRH : HasSubexponentialUpperBoundSeq scale RH)
    (hR : HasSubexponentialUpperBoundSeq scale R) :
    ∃ S : ℕ → ℝ, (∀ n, 0 ≤ S n) ∧ HasSubexponentialUpperBoundSeq scale S ∧
      ∀ n (δ : ℝ) (h : H) (v : cartanRootIdeal H),
        ‖(finBasis ℝ H).equivFun h‖ ≤ RH n →
        ‖(WordBasisSelections.basis M.letter M.wordList β).equivFun v‖ ≤
          R n * Real.exp (δ * scale n) →
        ‖(WordBasisSelections.basis M.letter M.wordList β).equivFun
          (cartanIdealAdjointAutomorphism T H (-h) (cartanIdealWeightDilation T H h v))‖ ≤
…

Mentions: OAI.PolycyclicRecognition.HasSubexponentialUpperBoundSeq, OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.WordBasisSelections.basis, OAI.PolycyclicRecognition.cartanIdealAdjointAutomorphism, OAI.PolycyclicRecognition.cartanIdealWeightDilation