PositiveDerivative.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.AffineBernstein.contDiffAt_gradient line 15
theorem OAI.AffineBernstein.inner_fderiv_gradient line 20

lemma OAI.AffineBernstein.injOn_of_positive_derivative line 36

Source documentation

Positive-definiteness of the derivative makes a map injective on a convex set, by strict monotonicity along every segment.

lemma injOn_of_positive_derivative {S : Set E} (hS : Convex ℝ S) {G : E → E}
    (hG : ∀ x ∈ S, DifferentiableAt ℝ G x)
    (hpos : ∀ x ∈ S, ∀ v : E, v ≠ 0 → 0 < inner ℝ (fderiv ℝ G x v) v) :
    Set.InjOn G S := by
…

lemma OAI.AffineBernstein.gradient_injOn_of_hessian_posDef line 72
Source documentation
The actual gradient of a strictly positive-Hessian function is injective; in particular this applies to every principal-coordinate slice in the source.
```
lemma gradient_injOn_of_hessian_posDef {n : ℕ} {Ω : Set (Space n)}
    (hΩ : IsOpen Ω) (hcv : Convex ℝ Ω) {u : Space n → ℝ}
    (hu : ContDiffOn ℝ ∞ u Ω) (hp : ∀ x ∈ Ω, (hessian u x).PosDef) :
    Set.InjOn (gradient u) Ω := by
…
```
Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian
lemma OAI.AffineBernstein.det_fderiv_gradient_eq_hessian line 85
Source documentation
The true Euclidean gradient has Jacobian determinant equal to the coordinate Hessian determinant, including dimension zero.
```
lemma det_fderiv_gradient_eq_hessian {n : ℕ} {u : Space n → ℝ} {x : Space n}
    (hu : ContDiffAt ℝ ∞ u x) :
    (fderiv ℝ (gradient u) x).det = (hessian u x).det := by
…
```
Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian

lemma OAI.AffineBernstein.integral_hessian_det_eq_gradient_volume line 103

Source documentation

Exact change of variables for the convex gradient map. This is the principal-minor argument used in bounds.tex; applying this result on each coordinate slice gives the claimed integral bound for that minor.

lemma integral_hessian_det_eq_gradient_volume {n : ℕ}
    {μ : Measure (Space n)} [μ.IsAddHaarMeasure]
    {Ω : Set (Space n)} (hΩ : IsOpen Ω) (hcv : Convex ℝ Ω) {u : Space n → ℝ}
    (hu : ContDiffOn ℝ ∞ u Ω) (hp : ∀ x ∈ Ω, (hessian u x).PosDef)
    {K : Set (Space n)} (hK : MeasurableSet K) (hKO : K ⊆ Ω) :
    (∫ x in K, (hessian u x).det ∂μ) = μ.real (gradient u '' K) := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian

lemma OAI.AffineBernstein.integral_hessian_det_le_image_bound line 125

Source documentation

A uniformly bounded gradient image gives a uniformly bounded Hessian Jacobian integral. No bound on the Hessian itself is needed.

lemma integral_hessian_det_le_image_bound {n : ℕ}
    {μ : Measure (Space n)} [μ.IsAddHaarMeasure]
    {Ω : Set (Space n)} (hΩ : IsOpen Ω) (hcv : Convex ℝ Ω) {u : Space n → ℝ}
    (hu : ContDiffOn ℝ ∞ u Ω) (hp : ∀ x ∈ Ω, (hessian u x).PosDef)
    {K B : Set (Space n)} (hK : MeasurableSet K) (hKO : K ⊆ Ω)
    (hB : μ B ≠ ⊤) (hbound : ∀ x ∈ K, gradient u x ∈ B) :
    (∫ x in K, (hessian u x).det ∂μ) ≤ μ.real B := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian