RescaledBasisChange.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Exponential margins between two rescalings of the same basis

theorem OAI.PolycyclicRecognition.repr_change_exponentialRescaleBasis line 14

Source documentation

Exact coordinate change between two exponential rescalings.

theorem repr_change_exponentialRescaleBasis (b : Basis J ℝ L)
    (s t : J → ℝ) (r : ℝ) (x : L) (j : J) :
    (exponentialRescaleBasis b s r).repr x j =
      (exponentialRescaleBasis b t r).repr x j * Real.exp (r * (t j - s j)) := by
…

Mentions: OAI.PolycyclicRecognition.exponentialRescaleBasis

theorem OAI.PolycyclicRecognition.norm_change_exponentialRescaleBasis_le line 29

Source documentation

A common difference between the exponents gives an exponential gain or loss in the whole coordinate maximum norm.

theorem norm_change_exponentialRescaleBasis_le [Fintype J]
    (b : Basis J ℝ L) (s t : J → ℝ) {r α : ℝ} (hr : 0 ≤ r)
    (hgap : ∀ j, t j - s j ≤ α) (x : L) :
    ‖(exponentialRescaleBasis b s r).equivFun x‖ ≤
      Real.exp (r * α) * ‖(exponentialRescaleBasis b t r).equivFun x‖ := by
…

Mentions: OAI.PolycyclicRecognition.exponentialRescaleBasis