BochnerShiftedQuadratic.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Shifted Hessian domination from the scalar dimensional Bochner bound

The same quadratic perturbation used for the unshifted Hessian works in the positive form augmented by a scalar metric shift. Thus the scalar finite-dimensional Bochner inequality suffices; a separate identification of the local dimension is not needed for this step.

theorem OAI.RegularPointCoordinates.finite_bochner_shift_nonneg line 18
Source documentation
Completing the square augments a finite-dimensional Bochner bound by an arbitrary scalar shift.
```
theorem finite_bochner_shift_nonneg (N B delta b : ℝ) (hN : 0<N)
    (hBE : delta^2≤N*B) : 0≤B-2*b*delta+N*b^2 := by
…
```

theorem OAI.RegularPointCoordinates.bochner_shifted_quadratic_perturbation_bound line 29

Source documentation

Quadratic perturbation in the augmented positive form gives the exact shifted directional Hessian bound. The source of the squared direction is explicitly retained in hdelta.

theorem bochner_shifted_quadratic_perturbation_bound {m : ℕ}
    (B : Euclidean m →ₗ[ℝ] Euclidean m →ₗ[ℝ] ℝ)
    (delta : Euclidean m →ₗ[ℝ] ℝ) (N : ℝ)
    (hsym : ∀ a b, B a b=B b a)
    (hshift : ∀ a b, 0≤B a a-2*b*delta a+N*b^2)
    (f g q : Euclidean m) (c s H k b : ℝ)
    (hfg : B f q=2*c*B f g+2*H)
    (hgq : B g q=2*c*B g g+2*k)
    (hqq : B q q=4*c^2*B g g+8*c*k+4*s^2)
    (hdelta : delta q=2*c*delta g+2*s) :
    (H-b*s)^2≤(B f f-2*b*delta f+N*b^2)*s^2 := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean