CartanProbeChainDilation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Exact translation of the normalized probe generator chains

theorem OAI.PolycyclicRecognition.CartanWordModel.probe_dilation_coordinate_norm line 22

Source documentation

The exact weight dilation preserves the coordinate bound when the reference template is translated by the pivot height.

theorem probe_dilation_coordinate_norm {E : Set W} (hE : IsCompact E) (hne : E.Nonempty)
    (w : W) (β : M.Bases) (r : ℝ) (v : cartanRootIdeal H) :
    ‖(M.boxBasis T hunimod eW ((fun x => x + w) '' E) β r).equivFun
      (cartanIdealWeightDilation T H (r • cartanHeightSection T H (eW.symm w)) v)‖ =
      ‖(M.boxBasis T hunimod eW E β r).equivFun v‖ := by
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.cartanIdealWeightDilation, OAI.PolycyclicRecognition.cartanHeightSection

theorem OAI.PolycyclicRecognition.CartanWordModel.probe_dilation_coefficient_bound line 34

Source documentation

The same dilation translates the generator amplitude exponent exactly.

theorem probe_dilation_coefficient_bound {E : Set W} (hE : IsCompact E) (hne : E.Nonempty)
    (w : W) (r t B : ℝ) (i : Fin M.letterCount)
    (ht : |t| ≤ B * Real.exp (r * (M.supportIn T hunimod eW).weightSupport E i)) :
    |t * Real.exp (r * M.weight i (cartanHeightSection T H (eW.symm w)))| ≤
      B * Real.exp (r * (M.supportIn T hunimod eW).weightSupport ((fun x => x + w) '' E) i) := by
…

Mentions: OAI.PolycyclicRecognition.cartanHeightSection

theorem OAI.PolycyclicRecognition.CartanWordModel.probe_dilation_generator_step line 59

Source documentation

Dilation carries each actual generator edge to the same letter with its explicitly rescaled coefficient.

theorem probe_dilation_generator_step
    (eN : cartanRootIdeal H ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, EN)) N)
    (ExpN : GroupLieAlgebra (𝓘(ℝ, EN)) N → N) (hExpN : IsGroupExponential ExpN)
    (hbij : Function.Bijective ExpN) (dynkin : NilpotentDynkinExpansionInput EN N)
    (h : H) (u v : cartanRootIdeal H) (i : Fin M.letterCount) (t : ℝ)
    (hedge : ExpN (eN v) = ExpN (eN u) * ExpN (eN (t • M.letter i))) :
    ExpN (eN (cartanIdealWeightDilation T H h v)) =
      ExpN (eN (cartanIdealWeightDilation T H h u)) *
        ExpN (eN ((t * Real.exp (M.weight i h)) • M.letter i)) := by
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput, OAI.PolycyclicRecognition.cartanIdealWeightDilation