BochnerQuadraticBound.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The quadratic perturbation estimate for a positive Bochner form

theorem OAI.RegularPointCoordinates.finite_positive_bilinear_cauchySchwarz line 12

theorem OAI.RegularPointCoordinates.bochner_quadratic_perturbation_bound line 28

Source documentation

Subtracting the linear part of a quadratic perturbation removes its value at the point. Positivity then gives the sharp directional Hessian bound; no positive-definiteness of the form is required.

theorem bochner_quadratic_perturbation_bound
    (B : Euclidean m →ₗ[ℝ] Euclidean m →ₗ[ℝ] ℝ)
    (hsym : ∀ a b, B a b=B b a) (hpos : ∀ a, 0≤B a a)
    (f g q : Euclidean m) (c s H k : ℝ)
    (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) :
    H^2≤B f f*s^2 := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean

theorem OAI.RegularPointCoordinates.bochnerRadonDensity_cauchySchwarz line 57
Source documentation
Cauchy–Schwarz holds outside one null set for every pair of real coordinate directions of the full Bochner density.
```
theorem bochnerRadonDensity_cauchySchwarz (M : PositiveBilinearMeasure X (Euclidean m)) :
    ∀ᵐ x ∂μ, ∀ a b : Euclidean m, (bochnerRadonDensity μ M x a b)^2 ≤
      bochnerRadonDensity μ M x a a*bochnerRadonDensity μ M x b b := by
…
```
Mentions: OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.bochnerRadonDensity