RescaledBasisScaleChange.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Changing the physical scale of one exponential basis

theorem OAI.PolycyclicRecognition.repr_scale_exponentialRescaleBasis line 13

theorem OAI.PolycyclicRecognition.norm_scale_exponentialRescaleBasis_le line 28

Source documentation

The exact change in scale is bounded by the largest change in a coordinate exponent. There is no asymptotic hypothesis in this estimate.

theorem norm_scale_exponentialRescaleBasis_le [Fintype J]
    (b : Basis J ℝ L) (c : J → ℝ) (r t A : ℝ)
    (hgap : ∀ j, (t - r) * c j ≤ A) (x : L) :
    ‖(exponentialRescaleBasis b c r).equivFun x‖ ≤
      Real.exp A * ‖(exponentialRescaleBasis b c t).equivFun x‖ := by
…

Mentions: OAI.PolycyclicRecognition.exponentialRescaleBasis