WordChartScaleTransition.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Exact coordinate and height identities between two chart scales

def OAI.PolycyclicRecognition.basisScaleTransition line 17
Source documentation
Coordinates of the same Lie-algebra point in the second scaled basis.
```
def basisScaleTransition (b : Basis J ℝ L) (cost : J → ℝ) (r t : ℝ) :
    (J → ℝ) ≃ₗ[ℝ] (J → ℝ) :=
…
```
theorem OAI.PolycyclicRecognition.basisScaleTransition_point line 22

theorem OAI.PolycyclicRecognition.norm_basisScaleTransition_le line 29

Source documentation

Enlarging a scale contracts all coordinates with nonnegative weight.

theorem norm_basisScaleTransition_le [Fintype J]
    (b : Basis J ℝ L) (cost : J → ℝ) (hcost : ∀ j, 0 ≤ cost j)
    {r t : ℝ} (hrt : r ≤ t) (z : J → ℝ) :
    ‖basisScaleTransition b cost r t z‖ ≤ ‖z‖ := by
…

Mentions: OAI.PolycyclicRecognition.basisScaleTransition

theorem OAI.PolycyclicRecognition.wordChartScaleTransition_height line 40

Source documentation

A bracket-killing height scales by the physical scale ratio, exactly.

theorem wordChartScaleTransition_height
    {I W : Type*} [Fintype I] [DecidableEq I] [AddCommGroup W] [Module ℝ W]
    (X : I → L) (S : Finset (FreeMagma I)) (β : WordBasisSelections X S)
    (height : L →ₗ[ℝ] W) (hkill : ∀ x y : L, height ⁅x, y⁆ = 0)
    {r t : ℝ} (hr : 0 < r) (ht : 0 < t) (z : Fin (finrank ℝ L) → ℝ) :
    let b := WordBasisSelections.basis X S β
…

Mentions: OAI.PolycyclicRecognition.WordBasisSelections, OAI.PolycyclicRecognition.WordBasisSelections.basis

theorem OAI.PolycyclicRecognition.scaled_profile_eq_of_chart_eq line 61

Source documentation

If the two charts represent the same point, their actual profiles agree after multiplication by the physical scale.

theorem scaled_profile_eq_of_chart_eq
    {G W Z : Type*} [Group G] [PseudoMetricSpace G]
    [NormedAddCommGroup W] [NormedSpace ℝ W]
    (map : G → W) (x k : G) {r t : ℝ} (hr : 0 < r) (ht : 0 < t)
    (φ ψ : Z → G) (z z' : Z) (hpoint : φ z = ψ z') :
    r • rescaledMapProfile map x k (Real.log r) φ z =
      t • rescaledMapProfile map x k (Real.log t) ψ z' := by
…

Mentions: OAI.PolycyclicRecognition.rescaledMapProfile