OAI/Analysis/MassAction/FiniteMinimum.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem326.eventually_slope_finset_inf'_gt line 17

   Source documentation

   A finite minimum has nonnegative lower right slope when every active branch has a nonnegative right derivative. Inactive branches need only be right-continuous.

   theorem eventually_slope_finset_inf'_gt
       {ι : Type uIota} {s : Finset ι} (hs : s.Nonempty)
       {f : ι → ℝ → ℝ} {x : ℝ}
       (hc : ∀ i ∈ s, ContinuousWithinAt (f i) (Ioi x) x)
       (hd : ∀ i ∈ s, f i x = s.inf' hs (fun j => f j x) →
         ∃ v : ℝ, 0 ≤ v ∧ HasDerivWithinAt (f i) v (Ici x) x)
       {r : ℝ} (hr : r < 0) :
       ∀ᶠ y in 𝓝[>] x,
         r < slope (fun t => s.inf' hs (fun i => f i t)) x y := by
   …

2. theorem OAI.Problem326.finset_inf'_initial_le line 56

   Source documentation

   Endpoint comparison for a finite minimum, using only derivatives of active branches. The right derivative is required at the left endpoint.

   theorem finset_inf'_initial_le
       {ι : Type uIota} {s : Finset ι} (hs : s.Nonempty)
       {f : ι → ℝ → ℝ} {a b : ℝ}
       (hc : ∀ i ∈ s, ContinuousOn (f i) (Icc a b))
       (hd : ∀ x ∈ Ico a b, ∀ i ∈ s,
         f i x = s.inf' hs (fun j => f j x) →
         ∃ v : ℝ, 0 ≤ v ∧ HasDerivWithinAt (f i) v (Ici x) x) :
       ∀ t ∈ Icc a b, s.inf' hs (fun i => f i a) ≤ s.inf' hs (fun i => f i t) := by
   …

3. theorem OAI.Problem326.monotoneOn_finset_inf'_of_active_right_deriv_nonneg line 87

   Source documentation

   A finite minimum is monotone when every active branch has nonnegative right derivative. No derivative is required of an inactive branch.

   theorem monotoneOn_finset_inf'_of_active_right_deriv_nonneg
       {ι : Type uIota} {s : Finset ι} (hs : s.Nonempty)
       {f : ι → ℝ → ℝ} {a b : ℝ}
       (hc : ∀ i ∈ s, ContinuousOn (f i) (Icc a b))
       (hd : ∀ x ∈ Ico a b, ∀ i ∈ s,
         f i x = s.inf' hs (fun j => f j x) →
         ∃ v : ℝ, 0 ≤ v ∧ HasDerivWithinAt (f i) v (Ici x) x) :
       MonotoneOn (fun t => s.inf' hs (fun i => f i t)) (Icc a b) := by
   …

4. theorem OAI.Problem326.monotoneOn_finset_inf'_of_active_deriv_nonneg line 103

   Source documentation

   Interior-derivative form: continuity handles both endpoints, so this applies to solution curves whose ODE is only assumed on an open interval.

   theorem monotoneOn_finset_inf'_of_active_deriv_nonneg
       {ι : Type uIota} {s : Finset ι} (hs : s.Nonempty)
       {f : ι → ℝ → ℝ} {a b : ℝ}
       (hc : ∀ i ∈ s, ContinuousOn (f i) (Icc a b))
       (hd : ∀ x ∈ Ioo a b, ∀ i ∈ s,
         f i x = s.inf' hs (fun j => f j x) →
         ∃ v : ℝ, 0 ≤ v ∧ HasDerivAt (f i) v x) :
       MonotoneOn (fun t => s.inf' hs (fun i => f i t)) (Icc a b) := by
   …