CoordinateInverseSections.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Continuous inverses for the normalized generator schemes

The amplitude differential is square. Its already proved surjectivity is therefore bijectivity, so compactness supplies a finite set of schemes with continuous inverse sections on one common coordinate ball.

theorem OAI.PolycyclicRecognition.exists_uniform_coordinate_inverse_sections line 24

Source documentation

Measurable endpoint coding for every actual normalized law: the inverse is continuous on the common ball, and all its amplitudes are bounded by one.

theorem exists_uniform_coordinate_inverse_sections {J : Type*} {c : ℕ}
    (a : DynkinCoefficients c 2) (b₀ : Basis J ℝ V) (w₀ : J → FreeMagma I) (C : ℝ) :
    ∃ (schemes : Finset ((Fin (finrank ℝ V) → List (I × ℝ)) ×
        (Fin (finrank ℝ V) → I))) (ε : ℝ), 0 < ε ∧
      ∀ p ∈ normalizedExponentialParameters a w₀ b₀ C,
        ∃ s ∈ schemes, ∃ σ : V → (Fin (finrank ℝ V) → ℝ),
          ContinuousOn σ (ball 0 ε) ∧ ∀ y ∈ ball (0 : V) ε,
            polynomialEndpointScheme a s.1 s.2 p (σ y) = y ∧ ‖σ y‖ < 1 := by
…

Mentions: OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.normalizedExponentialParameters, OAI.PolycyclicRecognition.polynomialEndpointScheme