Continuation.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.SepticProfile.RegularContinuation.exists_between_lower_equilibrium line 14

Source documentation

A strict moving lower fence and an invariant upper equilibrium suffice. An exponential strict upper fence is constructed from the compact Lipschitz constant, rather than assuming a continuation or a separation estimate.

theorem exists_between_lower_equilibrium {a b c d u0 : ℝ}
    (hab : a≤b) (hcd : c≤d)
    {f : ℝ×ℝ → ℝ} (hf : ContDiffOn ℝ 1 f (Icc a b ×ˢ Icc c d))
    (lo dlo : ℝ → ℝ)
    (hloder : ∀ t ∈ Icc a b, HasDerivAt lo (dlo t) t)
    (hlorange : ∀ t ∈ Icc a b, lo t ∈ Icc c d)
    (hlostrict : ∀ t ∈ Icc a b, dlo t<f (t,lo t))
    (heq : ∀ t ∈ Icc a b, f (t,d)=0)
    (hu0 : lo a≤u0) (hu0d : u0<d) :
    ∃ u : ℝ → ℝ, u a=u0 ∧ ContinuousOn u (Icc a b) ∧
      (∀ t ∈ Icc a b, lo t≤u t ∧ u t<d) ∧
      ∀ t ∈ Icc a b, HasDerivWithinAt u (f (t,u t)) (Icc a b) t := by
…