CoordinateChartSampling.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The coordinate maps of the actual two-factor chart samples

theorem OAI.PolycyclicRecognition.model_binary_dynkin line 16

Source documentation

A Lie-algebra identification transports the same binary Dynkin formula.

theorem model_binary_dynkin
    {L L' N : Type*} [LieRing L] [LieAlgebra ℝ L]
    [LieRing L'] [LieAlgebra ℝ L'] [Group N]
    (e : L ≃ₗ⁅ℝ⁆ L') (Exp : L' → N) {c : ℕ} (a : DynkinCoefficients c 2)
    (hm : ∀ x y, Exp (finiteDynkinPolynomial a ![x, y]) = Exp x * Exp y)
    (x y : L) :
    Exp (e (finiteDynkinPolynomial a ![x, y])) = Exp (e x) * Exp (e y) := by
…

Mentions: OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.finiteDynkinPolynomial

theorem OAI.PolycyclicRecognition.exp_basis_dynkinProduct line 31

Source documentation

The coordinate Dynkin product maps to the actual group product.

theorem exp_basis_dynkinProduct
    {L N : Type*} [LieRing L] [LieAlgebra ℝ L] [Group N]
    {n c : ℕ} (b : Basis (Fin n) ℝ L) (Exp : L → N)
    (a : DynkinCoefficients c 2)
    (hm : ∀ x y, Exp (finiteDynkinPolynomial a ![x, y]) = Exp x * Exp y)
    (x y : Fin n → ℝ) :
    Exp (b.equivFun.symm (dynkinProduct a (basisBracket b) x y)) =
      Exp (b.equivFun.symm x) * Exp (b.equivFun.symm y) := by
…

Mentions: OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.finiteDynkinPolynomial, OAI.PolycyclicRecognition.dynkinProduct, OAI.PolycyclicRecognition.basisBracket

def OAI.PolycyclicRecognition.coordinateChartPoint line 50

Source documentation

The chart sample uses the actual factor exponentials and includes the deterministic enlarged suffix.

def coordinateChartPoint (p : NormalizedPair G Λ) (x : G)
    (ι : N →* G) (κ : D →* G) (ExpN : LN → N) (ExpD : LD → D)
    (bN : Basis (Fin n) ℝ LN) (bD : Basis (Fin d) ℝ LD) (k : N)
    (z : (Fin n → ℝ) × (Fin d → ℝ)) : NormalizedPair G Λ :=
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair

theorem OAI.PolycyclicRecognition.coordinateChartPoint_right line 59

Source documentation

The second-factor coordinate translation is exactly the normalized action of the corresponding fixed group element.

theorem coordinateChartPoint_right
    (p : NormalizedPair G Λ) (x : G) (ι : N →* G) (κ : D →* G)
    (ExpN : LN → N) (ExpD : LD → D)
    (bN : Basis (Fin n) ℝ LN) (bD : Basis (Fin d) ℝ LD) (k : N)
    {c : ℕ} (a : DynkinCoefficients c 2)
    (hm : ∀ x y, ExpD (finiteDynkinPolynomial a ![x, y]) = ExpD x * ExpD y)
    (v : LD) (z : (Fin n → ℝ) × (Fin d → ℝ)) :
    (κ (ExpD v))⁻¹ • coordinateChartPoint p x ι κ ExpN ExpD bN bD k z =
      coordinateChartPoint p x ι κ ExpN ExpD bN bD k
        (z.1, dynkinProduct a (basisBracket bD) z.2 (bD.equivFun v)) := by
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.finiteDynkinPolynomial, OAI.PolycyclicRecognition.coordinateChartPoint, OAI.PolycyclicRecognition.dynkinProduct, OAI.PolycyclicRecognition.basisBracket

theorem OAI.PolycyclicRecognition.coordinateChartPoint_normal line 76

Source documentation

The first-factor move has precisely the suffix-conjugated coordinate parameter appearing in interior slack. Its expression is derived from the actual factor action, rather than assumed as a coordinate identity.

theorem coordinateChartPoint_normal
    (p : NormalizedPair G Λ) (x : G) (ι : N →* G) (κ : D →* G)
    (φ : D →* MulAut N)
    (hφ : ∀ d n, ι (φ d n) = κ d * ι n * (κ d)⁻¹)
    (ExpN : LN → N) (ExpD : LD → D) (logN : N → LN)
    (hlog : ∀ n, ExpN (logN n) = n)
    (bN : Basis (Fin n) ℝ LN) (bD : Basis (Fin d) ℝ LD) (k u : N)
    {c : ℕ} (a : DynkinCoefficients c 2)
    (hm : ∀ x y, ExpN (finiteDynkinPolynomial a ![x, y]) = ExpN x * ExpN y)
    (z : (Fin n → ℝ) × (Fin d → ℝ)) :
    (ι u)⁻¹ • coordinateChartPoint p x ι κ ExpN ExpD bN bD k z =
      coordinateChartPoint p x ι κ ExpN ExpD bN bD k
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.finiteDynkinPolynomial, OAI.PolycyclicRecognition.coordinateChartPoint

theorem OAI.PolycyclicRecognition.coordinateChartPoint_normal_of_exponential_action line 98

Source documentation

When the factor action on exponentials has been identified, its exact coordinate move is the double Dynkin product controlled by interior slack. No logarithm of a group product is left as an extra assumption.

theorem coordinateChartPoint_normal_of_exponential_action
    (p : NormalizedPair G Λ) (x : G) (ι : N →* G) (κ : D →* G)
    (φ : D →* MulAut N)
    (hφ : ∀ d n, ι (φ d n) = κ d * ι n * (κ d)⁻¹)
    (ExpN : LN → N) (ExpD : LD → D)
    (hneg : ∀ v, ExpN (-v) = (ExpN v)⁻¹)
    (A : LD → LN → LN)
    (hact : ∀ d v, φ (ExpD d) (ExpN v) = ExpN (A d v))
    (bN : Basis (Fin n) ℝ LN) (bD : Basis (Fin d) ℝ LD) (k v : LN)
    {c : ℕ} (a : DynkinCoefficients c 2)
    (hm : ∀ x y, ExpN (finiteDynkinPolynomial a ![x, y]) = ExpN x * ExpN y)
    (z : (Fin n → ℝ) × (Fin d → ℝ)) :
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.finiteDynkinPolynomial

theorem OAI.PolycyclicRecognition.continuous_coordinateChartPoint line 125

Source documentation

Continuity of the factor charts gives continuity of the joint sample.

theorem continuous_coordinateChartPoint [ProperSpace G]
    (p : NormalizedPair G Λ) (x : G) (ι : N →* G) (κ : D →* G)
    (ExpN : LN → N) (ExpD : LD → D)
    (bN : Basis (Fin n) ℝ LN) (bD : Basis (Fin d) ℝ LD) (k : N)
    (hN : Continuous (fun z => ι (ExpN (bN.equivFun.symm z))))
    (hD : Continuous (fun z => κ (ExpD (bD.equivFun.symm z)))) :
    Continuous (coordinateChartPoint p x ι κ ExpN ExpD bN bD k) := by
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.coordinateChartPoint