CompactTransverseCorrection.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Compact transverse correction from local defining functions, with the cutoffs constructed.

theorem OAI.ClosedSurfaceR4.TransverseSmallFunction.compact_transverse_correction line 16

Source documentation

Local defining functions on the support of the desired derivative suffice.

theorem compact_transverse_correction {K O : Set E} {T : E → ℝ} (v : E)
    (hK : IsCompact K) (hO : IsOpen O) (hKO : K ⊆ O) (hT : ContDiff ℝ ∞ T)
    (hlocal : ∀ p ∈ K ∩ tsupport T, ∃ U : Set E, IsOpen U ∧ p ∈ U ∧
      ∃ f : E → ℝ, ContDiff ℝ ∞ f ∧ (∀ x ∈ K ∩ U, f x = 0) ∧
        ∀ x ∈ U, fderiv ℝ f x v ≠ 0)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ H : E → ℝ, ContDiff ℝ ∞ H ∧ HasCompactSupport H ∧ tsupport H ⊆ O ∧
      (∀ x, |H x| < ε) ∧ ∀ x ∈ K, fderiv ℝ H x v = T x := by
…