OAI/Analysis/MassAction/ActiveBranchMinimum.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem326.eventually_lt_right_of_hasDerivAt_pos line 13

   Source documentation

   A positive derivative gives strict increase immediately to the right.

   lemma eventually_lt_right_of_hasDerivAt_pos {f : ℝ → ℝ} {f' t : ℝ}
       (hf : HasDerivAt f f' t) (hpos : 0 < f') :
       ∀ᶠ u in 𝓝[>] t, f t < f u := by
   …

2. lemma OAI.Problem326.finite_minimum_eventually_lt_right line 24

   Source documentation

   Finite lower envelopes increase to the right when every active branch has strictly positive derivative. Inactive branches only need continuity.

   lemma finite_minimum_eventually_lt_right {ι : Type uIota} (s : Finset ι)
       (hne : s.Nonempty) (f : ι → ℝ → ℝ) (t : ℝ)
       (hcont : ∀ i ∈ s, ContinuousWithinAt (f i) (Ioi t) t)
       (hderiv : ∀ i ∈ s, s.inf' hne (fun j => f j t) = f i t →
         ∃ v : ℝ, HasDerivAt (f i) v t ∧ 0 < v) :
       ∀ᶠ u in 𝓝[>] t, s.inf' hne (fun j => f j t) < s.inf' hne (fun j => f j u) := by
   …

3. lemma OAI.Problem326.finite_minimum_add_const line 42

   Source documentation

   Adding the same constant commutes with a finite minimum.

   lemma finite_minimum_add_const {ι : Type uIota} (s : Finset ι) (hne : s.Nonempty)
       (f : ι → ℝ) (c : ℝ) :
       s.inf' hne (fun i => f i + c) = s.inf' hne f + c := by
   …

4. theorem OAI.Problem326.finite_minimum_monotoneOn_Icc_of_active_deriv_nonneg line 54

   Source documentation

   A finite minimum whose active branches have nonnegative derivatives is nondecreasing. The left endpoint is included in the derivative hypothesis.

   theorem finite_minimum_monotoneOn_Icc_of_active_deriv_nonneg
       {ι : Type uIota} (s : Finset ι) (hne : s.Nonempty)
       (f : ι → ℝ → ℝ) (a b : ℝ)
       (hcont : ∀ i ∈ s, ContinuousOn (f i) (Icc a b))
       (hderiv : ∀ t ∈ Ico a b, ∀ i ∈ s,
         s.inf' hne (fun j => f j t) = f i t →
         ∃ v : ℝ, HasDerivAt (f i) v t ∧ 0 ≤ v) :
       MonotoneOn (fun t => s.inf' hne (fun i => f i t)) (Icc a b) := by
   …

5. theorem OAI.Problem326.finite_minimum_monotoneOn_Icc_of_active_deriv_nonneg_Ioo line 106

   Source documentation

   Endpoint-continuous version: no derivatives are required at the endpoints.

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