OAI/Analysis/AffineBernstein/TangentShiftCalculus.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.gradientSquared_eq_norm_fderiv line 18
2. lemma OAI.AffineBernstein.affineMaximalOn_add_affine line 23
3. def OAI.AffineBernstein.tangentShift line 39

   Source documentation

   Subtract the tangent plane and a positive section height; this does not alter the Hessian, hence preserves the original classical PDE.

   def tangentShift {n : ℕ} (f : Space n → ℝ) (a : Space n) (h : ℝ) (x : Space n) : ℝ :=
   …

   Mentions: OAI.AffineBernstein.Space

4. lemma OAI.AffineBernstein.tangentShift_eq_graphAffineFunction line 42
5. lemma OAI.AffineBernstein.contDiffOn_tangentShift line 49
6. lemma OAI.AffineBernstein.hessian_tangentShift line 55
7. lemma OAI.AffineBernstein.affineMaximalOn_tangentShift line 63
8. lemma OAI.AffineBernstein.fderiv_tangentShift line 69
9. lemma OAI.AffineBernstein.norm_fderiv_le_of_convex_bounded line 78