SmallTurnFunction.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Choose the small translation of the angle with a large derivative at both turns. Compactness bounds the endpoint-amplitude derivative before this choice.

theorem OAI.ClosedSurfaceR4.CollarVelocity.exists_small_turn_function line 18

Source documentation

The two endpoint derivatives can be made arbitrarily large while the translation itself is arbitrarily small. The geometric input is the checked local curve-equation form of the finite-curve correction lemma.

theorem exists_small_turn_function {K O P : Set Base}
    (hK : IsCompact K) (hO : IsOpen O) (hKO : K ⊆ O)
    (hP : P.Finite) (hPK : P ⊆ K)
    (hlocal : ∀ p ∈ K \ P, ∃ U : Set Base, IsOpen U ∧ p ∈ U ∧
      ∃ f : Base → ℝ, ContDiffOn ℝ ∞ f U ∧ (∀ x ∈ K ∩ U, f x = 0) ∧
        fderiv ℝ f p (0, 1) ≠ 0)
    {a A s : Base → ℝ} (ha : ContDiff ℝ ∞ a)
    (hA : ContDiff ℝ ∞ A) (hs : ContDiff ℝ ∞ s) (T : ℝ)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ h : Base → ℝ, ContDiff ℝ ∞ h ∧ HasCompactSupport h ∧ tsupport h ⊆ O ∧
      (∀ x, |h x| < ε) ∧ ∀ x ∈ K,
        T < fderiv ℝ (fun y => h y + blendedAmplitude (a y) (A y) (s y)) x (0, 1) ∧
…

Mentions: OAI.ClosedSurfaceR4.CollarVelocity.blendedAmplitude

theorem OAI.ClosedSurfaceR4.CollarVelocity.large_turns_after_reparametrization line 57

Source documentation

Any subsequently chosen positive density retains the large spatial derivatives.

theorem large_turns_after_reparametrization
    {a A s h : Base → ℝ} {K U : Set Base} {T : ℝ}
    (ha : ContDiff ℝ ∞ a) (hA : ContDiff ℝ ∞ A)
    (hs : ContDiff ℝ ∞ s) (hh : ContDiff ℝ ∞ h)
    (hU : IsOpen U) (hKU : K ⊆ U) {ρ : Base × ℝ → ℝ}
    (hρ : ContDiffOn ℝ ∞ ρ (U ×ˢ univ))
    (hpos : ∀ b ∈ U, ∀ t, 0 < ρ (b, t))
    (hper : ∀ b ∈ U, Function.Periodic (fun t => ρ (b, t)) 1)
    (hmass : ∀ b ∈ U, (∫ t in 0..1, ρ (b, t)) = 1)
    (hlarge : ∀ x ∈ K,
      T < fderiv ℝ (fun y => h y + blendedAmplitude (a y) (A y) (s y)) x (0, 1) ∧
      T < fderiv ℝ (fun y => h y - blendedAmplitude (a y) (A y) (s y)) x (0, 1)) :
…

Mentions: OAI.ClosedSurfaceR4.CollarVelocity.blendedAmplitude