ABPMatrix.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.AffineBernstein.det_le_det_mul_mixed_trace_pow line 17
lemma OAI.AffineBernstein.hessian_det_le_of_linearized_bound line 26
lemma OAI.AffineBernstein.hessian_posSemidef_of_localMin line 50

lemma OAI.AffineBernstein.abp_gradient_coverage line 56

Source documentation

The elementary supporting-plane step of ABP, without convex-envelope axioms.

lemma abp_gradient_coverage {n : ℕ} {f : Space n → ℝ} (hf : ContDiff ℝ ∞ f)
    {K : Set (Space n)} (hK : IsCompact K) {a : Space n} (ha : a ∈ K)
    {m R : ℝ} (hm : 0 < m) (hR : 0 < R)
    (hKR : K ⊆ Metric.closedBall a R) (hfa : f a ≤ -m)
    (hb : ∀ x ∈ K, x ∉ interior K → 0 ≤ f x) :
    ∀ p ∈ Metric.ball (0 : Space n) (m/(2*R)),
      ∃ x ∈ interior K, f x < 0 ∧ (hessian f x).PosSemidef ∧ gradient f x = p := by
…

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

def OAI.AffineBernstein.abpContactSet line 107
Source documentation
A closed set large enough to contain every lower supporting point.
```
def abpContactSet {n : ℕ} (K : Set (Space n)) (f : Space n → ℝ) : Set (Space n) :=
…
```
Mentions: OAI.AffineBernstein.Space
lemma OAI.AffineBernstein.isCompact_abpContactSet line 110
lemma OAI.AffineBernstein.abpContactSet_hessian line 121

theorem OAI.AffineBernstein.abp_contact_measure line 134

Source documentation

The measure-theoretic ABP estimate uses the genuine gradient Jacobian. No injectivity of the gradient or convexity of the tested function is assumed.

theorem abp_contact_measure {n : ℕ} {f : Space n → ℝ} (hf : ContDiff ℝ ∞ f)
    {K : Set (Space n)} (hK : IsCompact K) {a : Space n} (ha : a ∈ K)
    {m R D : ℝ} (hm : 0 < m) (hR : 0 < R)
    (hKR : K ⊆ Metric.closedBall a R) (hfa : f a ≤ -m)
    (hb : ∀ x ∈ K, x ∉ interior K → 0 ≤ f x)
    (hdet : ∀ x ∈ abpContactSet K f, (hessian f x).det ≤ D) :
    volume (Metric.ball (0 : Space n) (m/(2*R))) ≤
      ENNReal.ofReal D * volume (abpContactSet K f) := by
…

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