CompactCoordinatePullback.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Fixed smooth representatives of the coordinate transitions on each compact overlap, with exact local inverses and polynomial tensor transport.

theorem OAI.ClosedSurfaceR4.JetPolynomial.compact_coordinate_representatives line 16

Source documentation

Both coordinate maps can be extended off a compact overlap. Their actual inverse identities continue to hold as germs on a smaller open set.

theorem compact_coordinate_representatives
    (e : OpenPartialHomeomorph Base Base)
    (he : ContDiffOn ℝ ∞ e e.source) (hi : ContDiffOn ℝ ∞ e.symm e.target)
    {K : Set Base} (hK : IsCompact K) (hKe : K ⊆ e.source) :
    ∃ U : Set Base, IsOpen U ∧ K ⊆ U ∧ U ⊆ e.source ∧
      ∃ T S : Base → Base, ContDiff ℝ ∞ T ∧ ContDiff ℝ ∞ S ∧ EqOn T e U ∧
        (∀ x ∈ U, S (T x) = x) ∧
        (∀ x ∈ U, (T ∘ S) =ᶠ[𝓝 (T x)] id) := by
…

Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Base

theorem OAI.ClosedSurfaceR4.JetPolynomial.compact_tensor_polynomial_pullback line 54

Source documentation

Tensor polynomials have a fixed smooth expression on every compact coordinate overlap; the expression is chosen before the map being evaluated.

theorem compact_tensor_polynomial_pullback {n : ℕ}
    (P : Fin 3 → Fin n → Expression) (hP : ∀ k r, (P k r).SmoothCoeffs univ)
    (e : OpenPartialHomeomorph Base Base)
    (he : ContDiffOn ℝ ∞ e e.source) (hi : ContDiffOn ℝ ∞ e.symm e.target)
    {K : Set Base} (hK : IsCompact K) (hKe : K ⊆ e.source) :
    ∃ U : Set Base, IsOpen U ∧ K ⊆ U ∧ U ⊆ e.source ∧
        ∃ P' : Fin 3 → Fin n → Expression, (∀ k r, (P' k r).SmoothCoeffs univ) ∧
          ∀ (G H : Base → Space), ContDiff ℝ ∞ G → ContDiff ℝ ∞ H →
            (∀ x ∈ U, H x = G (e x)) → ∀ (ε t : ℝ) (x : Base), x ∈ U →
              Perturbation.coordinatePolynomialValue P' ε H t (planeCoordinateIsometry x) =
                tensorCoordinatePullbackValue e x
                  (Perturbation.coordinatePolynomialValue P ε G t
…

Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Expression, OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.Space, OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.coordinatePolynomialValue, OAI.ClosedSurfaceR4.JetPolynomial.planeCoordinateIsometry, OAI.ClosedSurfaceR4.JetPolynomial.tensorCoordinatePullbackValue