RescaledProfileLegs.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Physical height bounds on the actual profile legs

theorem OAI.PolycyclicRecognition.rescaled_profile_leg_bound line 16

Source documentation

Good profile values on the actual polynomial horizontal flow control precisely the physical one-parameter leg at scale exp s.

theorem rescaled_profile_leg_bound
    {L D N G W : Type*} [LieRing L] [LieAlgebra ℝ L]
    [Group D] [Group G] [NormedAddCommGroup W] [NormedSpace ℝ W]
    {n c : ℕ} (ExpD : L → D) (b : Basis (Fin n) ℝ L)
    (a : DynkinCoefficients c 2)
    (hm : ∀ x y, ExpD (finiteDynkinPolynomial a ![x, y]) = ExpD x * ExpD y)
    (ι : N → G) (κ : D →* G) (J : G → W) (x : G) (s : ℝ)
    (v : L) (z : Fin n → ℝ) (T : ℝ) (A : Set N)
    (flow : (Fin n → ℝ) × ℝ → Fin n → ℝ) (f : (Fin n → ℝ) → W) (ε : ℝ)
    (hgood : ∀ u ∈ A, ∀ t ∈ Icc (0 : ℝ) T,
      ‖rescaledMapProfile J x (ι u) s (fun y => κ (ExpD (b.equivFun.symm y)))
          (dynkinFlowMap a (basisBracket b) (b.equivFun (Real.exp s • v)) (z, t)) -
…

Mentions: OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.finiteDynkinPolynomial, OAI.PolycyclicRecognition.rescaledMapProfile, OAI.PolycyclicRecognition.dynkinFlowMap, OAI.PolycyclicRecognition.basisBracket

theorem OAI.PolycyclicRecognition.rescaled_profile_leg_image line 43

Source documentation

The preceding bound describes the image of the whole leg by the fixed limiting segment image, including every time used in the support visits.

theorem rescaled_profile_leg_image
    {L D N G W : Type*} [LieRing L] [LieAlgebra ℝ L]
    [Group D] [Group G] [NormedAddCommGroup W] [NormedSpace ℝ W]
    {n c : ℕ} (ExpD : L → D) (b : Basis (Fin n) ℝ L)
    (a : DynkinCoefficients c 2)
    (hm : ∀ x y, ExpD (finiteDynkinPolynomial a ![x, y]) = ExpD x * ExpD y)
    (ι : N → G) (κ : D →* G) (J : G → W) (x : G) (s : ℝ)
    (v : L) (z : Fin n → ℝ) (T : ℝ) (A : Set N)
    (flow : (Fin n → ℝ) × ℝ → Fin n → ℝ) (f : (Fin n → ℝ) → W) (ε : ℝ)
    (hgood : ∀ u ∈ A, ∀ t ∈ Icc (0 : ℝ) T,
      ‖rescaledMapProfile J x (ι u) s (fun y => κ (ExpD (b.equivFun.symm y)))
          (dynkinFlowMap a (basisBracket b) (b.equivFun (Real.exp s • v)) (z, t)) -
…