RayQuotientContraction.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Contraction on the constructed positive-ray quotient

This proves the linear logarithmic estimate underlying boundary.tex, equation (quotient-contraction). The basis is made of actual pure bracket words in the quotient by the mixed-word ideal. Its scalar weights are positive multiples of the chosen ray, while its residual Cartan action has the already-proved polynomial bound.

theorem OAI.PolycyclicRecognition.pure_ray_word_exponent line 26

Source documentation

A pure word in positive multiples of one form has a strictly positive multiple of that form as its total exponent.

theorem pure_ray_word_exponent
    {I V : Type*} [Fintype I] [DecidableEq I] [AddCommGroup V] [Module ℝ V]
    (α : V →ₗ[ℝ] ℝ) (weight : I → V →ₗ[ℝ] ℝ) (w : FreeMagma I)
    (hw : ¬IsMixedWord (fun i => weight i ∉ positiveWeightRay α) w) :
    ∃ c : ℝ, 0 < c ∧ ∀ v, bracketWordExponent (fun i => weight i v) w = c * α v := by
…

Mentions: OAI.PolycyclicRecognition.IsMixedWord, OAI.PolycyclicRecognition.positiveWeightRay, OAI.PolycyclicRecognition.bracketWordExponent

theorem OAI.PolycyclicRecognition.exists_pos_le_finite_family line 47
Source documentation
A finite family of positive numbers has one strictly positive lower bound, including when the index type is empty.
```
theorem exists_pos_le_finite_family {J : Type*} [Fintype J]
    (a : J → ℝ) (ha : ∀ j, 0 < a j) :
    ∃ c : ℝ, 0 < c ∧ ∀ j, c ≤ a j := by
…
```

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_ray_dilation_bound line 71

Source documentation

The exact dilation contracts a pure-word ray quotient basis at a common exponential rate in every nonpositive ray direction.

theorem exists_ray_dilation_bound
    (α : H →ₗ[ℝ] ℝ) {J : Type*} [Fintype J]
    (b : Basis J ℝ ((cartanRootIdeal H) ⧸ M.coneWordIdeal (positiveWeightRay α)))
    (words : J → FreeMagma (Fin M.letterCount))
    (hpure : ∀ j, ¬IsMixedWord
      (fun i => (M.weight i : H →ₗ[ℝ] ℝ) ∉ positiveWeightRay α) (words j))
    (hb : ∀ j, (M.coneWordIdeal (positiveWeightRay α)).toSubmodule.mkQ
      (evalBracketWord M.letter (words j)) = b j) :
    ∃ c : ℝ, 0 < c ∧ ∀ (h : H), α h ≤ 0 →
      ∀ v : (cartanRootIdeal H) ⧸ M.coneWordIdeal (positiveWeightRay α),
      ‖b.equivFun ((M.coneWordIdeal (positiveWeightRay α)).toSubmodule.mapQ
        (M.coneWordIdeal (positiveWeightRay α)).toSubmodule
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.positiveWeightRay, OAI.PolycyclicRecognition.IsMixedWord, OAI.PolycyclicRecognition.evalBracketWord

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_ray_quotient_contraction line 120

Source documentation

The actual Cartan action on the quotient by the positive-ray mixed-word ideal has polynomial times exponential contraction.

theorem exists_ray_quotient_contraction (α : H →ₗ[ℝ] ℝ) :
    ∃ (b : Basis
        (Fin (finrank ℝ ((cartanRootIdeal H) ⧸ M.coneWordIdeal (positiveWeightRay α))))
        ℝ ((cartanRootIdeal H) ⧸ M.coneWordIdeal (positiveWeightRay α)))
      (A : ℝ) (p : ℕ) (c : ℝ),
      0 ≤ A ∧ 0 < c ∧ ∀ (h : H), α h ≤ 0 →
        ∀ v : (cartanRootIdeal H) ⧸ M.coneWordIdeal (positiveWeightRay α),
        ‖b.equivFun (M.coneAdjointAutomorphism T (positiveWeightRay α)
          (positiveWeightRay_add α) h v)‖ ≤
        A * (1 + ‖(Module.finBasis ℝ H).equivFun h‖) ^ p *
          Real.exp (c * α h) * ‖b.equivFun v‖ := by
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.positiveWeightRay, OAI.PolycyclicRecognition.positiveWeightRay_add

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_summable_ray_quotient_bound line 158

Source documentation

Polynomially bounded Cartan parameters with uniformly negative linear ray height give one summable bound on the images of every bounded set in the actual quotient. The parameter type allows a whole family of paths.

theorem exists_summable_ray_quotient_bound
    (α : H →ₗ[ℝ] ℝ) {P : Type*} (h : P → ℕ → H)
    (K R δ : ℝ) (q : ℕ) (hK : 0 ≤ K) (hR : 0 ≤ R) (hδ : 0 < δ)
    (hbound : ∀ x n, ‖(Module.finBasis ℝ H).equivFun (h x n)‖ ≤
      K * (1 + (n : ℝ)) ^ q)
    (hheight : ∀ x n, α (h x n) ≤ -δ * n) :
    ∃ (b : Basis
        (Fin (finrank ℝ ((cartanRootIdeal H) ⧸ M.coneWordIdeal (positiveWeightRay α))))
        ℝ ((cartanRootIdeal H) ⧸ M.coneWordIdeal (positiveWeightRay α)))
      (C : ℝ) (m : ℕ) (c : ℝ),
      0 ≤ C ∧ 0 < c ∧
      Summable (fun n : ℕ => C * (1 + (n : ℝ)) ^ m * Real.exp (-c * n)) ∧
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.positiveWeightRay