OAI/GroupTheory/PolycyclicRecognition/Algebra/PositiveRescaling.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exponentialRescaleBasis_coordinates_tendsto_zero line 14

   Source documentation

   Every fixed logarithmic displacement tends to zero when all coordinate weights are positive. The scale parameter here is logarithmic.

   theorem exponentialRescaleBasis_coordinates_tendsto_zero
       {L J : Type*} [LieRing L] [LieAlgebra ℝ L] [Fintype J]
       (b : Basis J ℝ L) (cost : J → ℝ) (hcost : ∀ j, 0 < cost j) (x : L) :
       Tendsto (fun r : ℝ => (exponentialRescaleBasis b cost r).equivFun x)
         atTop (𝓝 0) := by
   …

   Mentions: OAI.PolycyclicRecognition.exponentialRescaleBasis

2. theorem OAI.PolycyclicRecognition.exponentialRescaleBasis_nonneg_coordinates_tendsto_zero line 36

   Source documentation

   Replacing a negative logarithmic scale by zero does not alter its large-scale limit and gives a family defined with nonnegative scales.

   theorem exponentialRescaleBasis_nonneg_coordinates_tendsto_zero
       {L J : Type*} [LieRing L] [LieAlgebra ℝ L] [Fintype J]
       (b : Basis J ℝ L) (cost : J → ℝ) (hcost : ∀ j, 0 < cost j) (x : L) :
       Tendsto (fun r : ℝ => (exponentialRescaleBasis b cost (max r 0)).equivFun x)
         atTop (𝓝 0) := by
   …

   Mentions: OAI.PolycyclicRecognition.exponentialRescaleBasis