LocalVelocity.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.AffineBernstein.contDiff_indicator_vector_of_compact line 11

lemma OAI.AffineBernstein.smooth_local_velocity_transport line 36

Source comment

Push a compactly supported smooth local velocity through a genuine smooth coordinate inverse and extend by zero. Smoothness at the chart boundary is proved, not an extra assumption on the transported velocity.

lemma smooth_local_velocity_transport {E F G : Type*}
    [NormedAddCommGroup E] [NormedSpace ℝ E]
    [NormedAddCommGroup F] [NormedSpace ℝ F]
    [NormedAddCommGroup G] [NormedSpace ℝ G]
    (φ : OpenPartialHomeomorph E F) (hψ : ContDiffOn ℝ ∞ φ.symm φ.target)
    {K : Set E} (hK : IsCompact K) (hKφ : K ⊆ φ.source)
    {V : E → G} (hV : ContDiffOn ℝ ∞ V φ.source) (hVK : tsupport V ⊆ K) :
    ∃ W : F → G, ContDiff ℝ ∞ W ∧ tsupport W ⊆ φ '' K ∧
      ∀ x ∈ φ.source, W (φ x) = V x := by
…

lemma OAI.AffineBernstein.smooth_chart_jacobian_ne line 64

theorem OAI.AffineBernstein.affineMaximal_local_chart_stationary line 85

Source comment

Every compact smooth ambient velocity in a local chart is a genuine compact smooth graph velocity. This removes the extension requirement from the coordinate stationarity theorem.

theorem affineMaximal_local_chart_stationary {n : ℕ}
    {Ω K : Set (Space n)} (hΩ : IsOpen Ω) (hK : IsCompact K)
    (φ : OpenPartialHomeomorph (Space n) (Space n))
    (hφ : ContDiffOn ℝ ∞ φ φ.source) (hψ : ContDiffOn ℝ ∞ φ.symm φ.target)
    (hKφ : K ⊆ φ.source) (hφΩ : φ.target ⊆ Ω)
    {u : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω)
    (hp : ∀ x ∈ Ω, (hessian u x).PosDef) (hm : AffineMaximalOn Ω u)
    {V : Space n → Space n × ℝ} (hV : ContDiffOn ℝ ∞ V φ.source)
    (hVK : tsupport V ⊆ K)
    (L : (Space n × ℝ) ≃L[ℝ] (Space n × ℝ)) (v : Space n × ℝ) :
    ∃ (β : Space n → ℝ) (a : Fin n → Space n → ℝ),
      ContDiff ℝ ∞ β ∧ (∀ i, ContDiff ℝ ∞ (a i)) ∧
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.AffineMaximalOn