OAI/Analysis/AffineBernstein/ActualBaseMinors.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.AffineBernstein.norm_gradient_le_of_convex_bounded line 18

    Source comment

    A bounded convex function on a full larger ball has bounded actual Euclidean gradient at its center. No derivative estimate is assumed.
    lemma norm_gradient_le_of_convex_bounded {Ω : Set E} {f : E → ℝ}
    (hc : ConvexOn ℝ Ω f) {x : E} (hx : x ∈ Ω) (hd : DifferentiableAt ℝ f x)
    {r M : ℝ} (hr : 0 < r) (hM : 0 ≤ M)
    (hball : Metric.closedBall x r ⊆ Ω) (hb : ∀ y ∈ Ω, |f y| ≤ M) :
    ‖gradient f x‖ ≤ 2*M/r := by
…
  2. lemma OAI.AffineBernstein.hessian_neg line 50
  3. lemma OAI.AffineBernstein.tubeBaseMatrix_basisFun line 56
  4. theorem OAI.AffineBernstein.affineEpigraph_base_minors_bound line 71

    Source comment

    The uniform large-principal-minor bound for the actual negative support of an affine epigraph. The larger base domain supplies the gradient bound; hence no derivative or determinant bound is added as a hypothesis.
    theorem affineEpigraph_base_minors_bound {n k : ℕ}
    {Ω : Set (Space n)} (hΩ : IsOpen Ω) (hcv : Convex ℝ Ω) {u : Space n → ℝ}
    (hu : ContDiffOn ℝ ∞ u Ω) (hp : ∀ x ∈ Ω, (hessian u x).PosDef)
    (a : Space n × ℝ) (L : (Space k × E) ≃L[ℝ] (Space n × ℝ))
    {D : Set (Space k)} (hD : IsOpen D) (hcD : Convex ℝ D)
    (hK : ∀ s ∈ D, IsCompact {y | (s,y) ∈ affineEpigraphPullback Ω u a L})
    (hzero : ∀ s ∈ D, (0:E) ∈ interior {y | (s,y) ∈ affineEpigraphPullback Ω u a L})
    {e : E} (he : e ≠ 0) {Q : Set (Space k)} (hQ : MeasurableSet Q) (hQD : Q ⊆ D)
    {r M R : ℝ} (hr : 0 < r) (hM : 0 ≤ M)
    (hball : ∀ s ∈ Q, Metric.closedBall s r ⊆ D)
    (hbound : ∀ s ∈ D,
      |homogeneousSupport {y | (s,y) ∈ affineEpigraphPullback Ω u a L} e| ≤ M)
…

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

  5. lemma OAI.AffineBernstein.homogeneousSupport_abs_le_of_radius line 122
  6. lemma OAI.AffineBernstein.homogeneousSupport_ge_of_ball line 131
  7. theorem OAI.AffineBernstein.affineEpigraph_base_minors_of_fiber_radius line 142

    Source comment

    Fully geometric formulation of the actual large-minor estimate: only the fibers' position in a fixed ball and a base collar are needed.
    theorem affineEpigraph_base_minors_of_fiber_radius {n k : ℕ}
    {Ω : Set (Space n)} (hΩ : IsOpen Ω) (hcv : Convex ℝ Ω) {u : Space n → ℝ}
    (hu : ContDiffOn ℝ ∞ u Ω) (hp : ∀ x ∈ Ω, (hessian u x).PosDef)
    (a : Space n × ℝ) (L : (Space k × E) ≃L[ℝ] (Space n × ℝ))
    {D : Set (Space k)} (hD : IsOpen D) (hcD : Convex ℝ D)
    (hK : ∀ s ∈ D, IsCompact {y | (s,y) ∈ affineEpigraphPullback Ω u a L})
    (hzero : ∀ s ∈ D, (0:E) ∈ interior {y | (s,y) ∈ affineEpigraphPullback Ω u a L})
    {e : E} (he : ‖e‖ = 1) {Q : Set (Space k)} (hQ : MeasurableSet Q) (hQD : Q ⊆ D)
    {r M R : ℝ} (hr : 0 < r) (hM : 0 ≤ M)
    (hball : ∀ s ∈ Q, Metric.closedBall s r ⊆ D)
    (hbound : ∀ s ∈ D, ∀ y : E, (s,y) ∈ affineEpigraphPullback Ω u a L → ‖y‖ ≤ M)
    (hR : ∀ s ∈ Q, ‖s‖ ≤ R) :
…

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