NilpotentSectionRemainder.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Polynomial bounds for the actual ideal section remainder

The remainder of an exponential after removing its pure quotient section is computed with the finite BCH formula. Its ideal coordinates have a polynomial bound in the original logarithm. No box comparison is assumed.

theorem OAI.PolycyclicRecognition.exponentialRescaleBasis_zero line 23

theorem OAI.PolycyclicRecognition.quotient_section_coordinate_norm_le line 30

Source documentation

Removing all ideal coordinates is a contraction in the adapted norm.

theorem quotient_section_coordinate_norm_le (v : V) :
    ‖(basisWithQuotientLifts U.toSubmodule bI bQ lift hlift).equivFun
      (quotientLinearSection U bQ lift (U.toSubmodule.mkQ v))‖ ≤
    ‖(basisWithQuotientLifts U.toSubmodule bI bQ lift hlift).equivFun v‖ := by
…

Mentions: OAI.PolycyclicRecognition.basisWithQuotientLifts, OAI.PolycyclicRecognition.quotientLinearSection

theorem OAI.PolycyclicRecognition.section_remainder_mem_ideal line 61
Source documentation
This is the actual kernel coordinate, not a freely selected small lift.
```
theorem section_remainder_mem_ideal (v : V) :
    finiteDynkinPolynomial coeff
      ![v, -quotientLinearSection U bQ lift (U.toSubmodule.mkQ v)] ∈ U := by
…
```
Mentions: OAI.PolycyclicRecognition.finiteDynkinPolynomial, OAI.PolycyclicRecognition.quotientLinearSection
def OAI.PolycyclicRecognition.sectionDynkinConstant line 76
Source documentation
The product constant depends on dimension, nilpotence degree, and a uniform bracket bound, rather than on the chosen basis.
```
def sectionDynkinConstant (d c : ℕ) (C : ℝ) : ℝ :=
…
```

theorem OAI.PolycyclicRecognition.section_remainder_polynomial_bound line 81

Source documentation

The same fixed polynomial controls the ideal remainder of every log.

theorem section_remainder_polynomial_bound (C : ℝ) (hC : 0 ≤ C)
    (hbr : ∀ i j k, |(basisWithQuotientLifts U.toSubmodule bI bQ lift hlift).repr
      ⁅basisWithQuotientLifts U.toSubmodule bI bQ lift hlift i,
        basisWithQuotientLifts U.toSubmodule bI bQ lift hlift j⁆ k| ≤ C) :
    ∀ R : ℝ, 0 ≤ R → ∀ v : V,
      ‖(basisWithQuotientLifts U.toSubmodule bI bQ lift hlift).equivFun v‖ ≤ R →
      ∃ u : U,
        ExpN (u : V) = ExpN v *
          (ExpN (quotientLinearSection U bQ lift (U.toSubmodule.mkQ v)))⁻¹ ∧
        ‖bI.equivFun u‖ ≤ sectionDynkinConstant (Fintype.card (I ⊕ J)) c C * (1 + R) ^ c := by
…

Mentions: OAI.PolycyclicRecognition.basisWithQuotientLifts, OAI.PolycyclicRecognition.quotientLinearSection, OAI.PolycyclicRecognition.sectionDynkinConstant

theorem OAI.PolycyclicRecognition.section_error_factorization_bound line 123

Source documentation

Factor a pure section followed by an arbitrary small logarithmic error. Both new coordinates have polynomial bounds, even when the new quotient coordinate leaves a subexponential ball.

theorem section_error_factorization_bound (C : ℝ) (hC : 0 ≤ C)
    (hbr : ∀ i j k, |(basisWithQuotientLifts U.toSubmodule bI bQ lift hlift).repr
      ⁅basisWithQuotientLifts U.toSubmodule bI bQ lift hlift i,
        basisWithQuotientLifts U.toSubmodule bI bQ lift hlift j⁆ k| ≤ C) :
    ∀ R : ℝ, 0 ≤ R →
      ∀ (q : V ⧸ U.toSubmodule) (e : V),
        ‖bQ.equivFun q‖ ≤ R →
        ‖(basisWithQuotientLifts U.toSubmodule bI bQ lift hlift).equivFun e‖ ≤ R →
        ∃ (u : U) (q' : V ⧸ U.toSubmodule),
          ExpN (quotientLinearSection U bQ lift q) * ExpN e =
            ExpN (u : V) * ExpN (quotientLinearSection U bQ lift q') ∧
          ‖bI.equivFun u‖ ≤
…

Mentions: OAI.PolycyclicRecognition.basisWithQuotientLifts, OAI.PolycyclicRecognition.quotientLinearSection