|
| 1 | +/- |
| 2 | +Copyright (c) 2025 Michael R. Douglas. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Michael R. Douglas |
| 5 | +-/ |
| 6 | +module |
| 7 | + |
| 8 | +public import Mathlib.Analysis.Calculus.ContDiff.Operations |
| 9 | +public import Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas |
| 10 | + |
| 11 | +/-! |
| 12 | +# Absolutely monotone functions |
| 13 | +
|
| 14 | +A function `f : ℝ → ℝ` is *absolutely monotone* on a set `s` if its iterated derivatives are all |
| 15 | +nonnegative on `s`. |
| 16 | +
|
| 17 | +## Main definitions |
| 18 | +
|
| 19 | +* `AbsolutelyMonotoneOn` — there exists a Taylor series for `f` on `s` with nonnegative terms at |
| 20 | + each point of `s`. |
| 21 | +
|
| 22 | +## Main results |
| 23 | +
|
| 24 | +* `AbsolutelyMonotoneOn.contDiffOn` — the function is `C^∞` on `s`. |
| 25 | +* `AbsolutelyMonotoneOn.of_contDiff` — a globally `C^∞` function with nonnegative iterated |
| 26 | + derivatives on `s` is absolutely monotone on `s`. |
| 27 | +* `AbsolutelyMonotoneOn.iff_iteratedDerivWithin_nonneg` — under `UniqueDiffOn`, the definition |
| 28 | + is equivalent to `f` being `C^∞` on `s` with every iterated derivative within `s` nonnegative. |
| 29 | +* `AbsolutelyMonotoneOn.add` — closure under addition. |
| 30 | +* `AbsolutelyMonotoneOn.smul` — closure under nonnegative scalar multiplication. |
| 31 | +
|
| 32 | +## Implementation |
| 33 | +
|
| 34 | +The precise definition is phrased via the existence of a Taylor series with nonnegative terms |
| 35 | +(`HasFTaylorSeriesUpToOn`) rather than via `iteratedDerivWithin`. This avoids forcing a |
| 36 | +`UniqueDiffOn s` hypothesis on every result: without `UniqueDiffOn`, "the" iterated derivative |
| 37 | +within `s` is not canonical, but the existence of a Taylor series is intrinsic to `f` and `s`. |
| 38 | +When `s` does satisfy `UniqueDiffOn`, the condition reduces to `f` being `C^∞` on `s` with every |
| 39 | +iterated derivative within `s` nonnegative. |
| 40 | +
|
| 41 | +## References |
| 42 | +
|
| 43 | +* [D. V. Widder, *The Laplace Transform*][widder1941] |
| 44 | +-/ |
| 45 | + |
| 46 | +public section |
| 47 | + |
| 48 | +open Set Filter |
| 49 | +open scoped ContDiff |
| 50 | + |
| 51 | +/-- A function `f : ℝ → ℝ` is **absolutely monotone on a set `s`** if, heuristically, all |
| 52 | +iterated derivatives of `f` on `s` are nonnegative. For technical reasons related to unique |
| 53 | +differentiability, the precise definition is phrased as the existence of a Taylor series for |
| 54 | +`f` on `s` whose `n`th term, evaluated at the all-ones tuple, is nonnegative for every `n` and |
| 55 | +every `x ∈ s`. See `AbsolutelyMonotoneOn.iff_iteratedDerivWithin_nonneg` for the equivalence |
| 56 | +under `UniqueDiffOn`. -/ |
| 57 | +def AbsolutelyMonotoneOn (f : ℝ → ℝ) (s : Set ℝ) : Prop := |
| 58 | + ∃ p : ℝ → FormalMultilinearSeries ℝ ℝ ℝ, |
| 59 | + HasFTaylorSeriesUpToOn ∞ f p s ∧ |
| 60 | + ∀ (n : ℕ) ⦃x : ℝ⦄, x ∈ s → 0 ≤ p x n fun _ ↦ (1 : ℝ) |
| 61 | + |
| 62 | +namespace AbsolutelyMonotoneOn |
| 63 | + |
| 64 | +variable {f g : ℝ → ℝ} {s : Set ℝ} |
| 65 | + |
| 66 | +/-- An absolutely monotone function on `s` is `C^∞` on `s`. -/ |
| 67 | +theorem contDiffOn (hf : AbsolutelyMonotoneOn f s) : ContDiffOn ℝ ∞ f s := by |
| 68 | + obtain ⟨_, hp, _⟩ := hf |
| 69 | + exact hp.contDiffOn |
| 70 | + |
| 71 | +/-- A globally `C^∞` function whose iterated derivatives are nonnegative on `s` is absolutely |
| 72 | +monotone on `s`. The set `s` need *not* satisfy `UniqueDiffOn`. -/ |
| 73 | +theorem of_contDiff (hf : ContDiff ℝ ∞ f) (h : ∀ n : ℕ, ∀ x ∈ s, 0 ≤ iteratedDeriv n f x) : |
| 74 | + AbsolutelyMonotoneOn f s := by |
| 75 | + refine ⟨ftaylorSeries ℝ f, (hf.ftaylorSeries).hasFTaylorSeriesUpToOn s, fun n x hx => ?_⟩ |
| 76 | + exact iteratedDeriv_eq_iteratedFDeriv (𝕜 := ℝ) (f := f) ▸ h n x hx |
| 77 | + |
| 78 | +/-- Under `UniqueDiffOn`, a Taylor witness for an absolutely monotone function agrees with |
| 79 | +`iteratedDerivWithin`, so the latter is nonnegative on `s`. -/ |
| 80 | +theorem iteratedDerivWithin_nonneg (hf : AbsolutelyMonotoneOn f s) (hs : UniqueDiffOn ℝ s) |
| 81 | + (n : ℕ) {x : ℝ} (hx : x ∈ s) : 0 ≤ iteratedDerivWithin n f s x := by |
| 82 | + obtain ⟨p, hp, hp_nn⟩ := hf |
| 83 | + have heq : p x n = iteratedFDerivWithin ℝ n f s x := |
| 84 | + hp.eq_iteratedFDerivWithin_of_uniqueDiffOn (mod_cast le_top) hs hx |
| 85 | + rw [iteratedDerivWithin_eq_iteratedFDerivWithin, ← heq] |
| 86 | + exact hp_nn n hx |
| 87 | + |
| 88 | +/-- Under `UniqueDiffOn`, a function is absolutely monotone on `s` iff it is `C^∞` on `s` with |
| 89 | +every iterated derivative within `s` nonnegative. -/ |
| 90 | +theorem iff_iteratedDerivWithin_nonneg (hs : UniqueDiffOn ℝ s) : |
| 91 | + AbsolutelyMonotoneOn f s ↔ |
| 92 | + ContDiffOn ℝ ∞ f s ∧ ∀ n : ℕ, ∀ x ∈ s, 0 ≤ iteratedDerivWithin n f s x := by |
| 93 | + refine ⟨fun hf => ⟨hf.contDiffOn, fun n x hx => hf.iteratedDerivWithin_nonneg hs n hx⟩, ?_⟩ |
| 94 | + rintro ⟨hcont, hnn⟩ |
| 95 | + refine ⟨ftaylorSeriesWithin ℝ f s, hcont.ftaylorSeriesWithin hs, fun n x hx => ?_⟩ |
| 96 | + exact iteratedDerivWithin_eq_iteratedFDerivWithin (𝕜 := ℝ) (f := f) (s := s) ▸ hnn n x hx |
| 97 | + |
| 98 | +/-! ### Closure properties -/ |
| 99 | + |
| 100 | +/-- The sum of two absolutely monotone functions is absolutely monotone. -/ |
| 101 | +theorem add (hf : AbsolutelyMonotoneOn f s) (hg : AbsolutelyMonotoneOn g s) : |
| 102 | + AbsolutelyMonotoneOn (f + g) s := by |
| 103 | + obtain ⟨p, hp, hp_nn⟩ := hf |
| 104 | + obtain ⟨q, hq, hq_nn⟩ := hg |
| 105 | + refine ⟨p + q, hp.add hq, fun n x hx => ?_⟩ |
| 106 | + simp only [Pi.add_apply, FormalMultilinearSeries.add_apply, |
| 107 | + ContinuousMultilinearMap.add_apply] |
| 108 | + exact add_nonneg (hp_nn n hx) (hq_nn n hx) |
| 109 | + |
| 110 | +/-- A nonnegative scalar multiple of an absolutely monotone function is absolutely monotone. -/ |
| 111 | +theorem smul {c : ℝ} (hf : AbsolutelyMonotoneOn f s) (hc : 0 ≤ c) : |
| 112 | + AbsolutelyMonotoneOn (c • f) s := by |
| 113 | + obtain ⟨p, hp, hp_nn⟩ := hf |
| 114 | + -- Witness: post-composition by the CLM `y ↦ c * y`. |
| 115 | + set T : ℝ →L[ℝ] ℝ := c • ContinuousLinearMap.id ℝ ℝ with hT |
| 116 | + have hcomp : (T ∘ f) = c • f := by ext x; simp [hT, smul_eq_mul] |
| 117 | + refine ⟨_, hcomp ▸ hp.continuousLinearMap_comp T, fun n x hx => ?_⟩ |
| 118 | + simp only [ContinuousLinearMap.compContinuousMultilinearMap_coe, Function.comp_apply, hT, |
| 119 | + ContinuousLinearMap.smul_apply, ContinuousLinearMap.id_apply, smul_eq_mul] |
| 120 | + exact mul_nonneg hc (hp_nn n hx) |
| 121 | + |
| 122 | +end AbsolutelyMonotoneOn |
0 commit comments