BochnerDensityQuadratic.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A sharp directional bound from the full quadratic product identities

theorem OAI.RegularPointCoordinates.bochner_measure_quadratic_bound line 20

Source documentation

The three product identities for a direction and its square imply the sharp bound for the first Hessian action. The positive form is the actual density of the same full Bochner measure.

theorem bochner_measure_quadratic_bound (M : PositiveBilinearMeasure X (Euclidean m))
    (v w z : Euclidean m) (χ : X →ᵇ ℝ) (Hv Hw Hz s : X → ℝ)
    (hHv : Integrable Hv μ) (hHw : Integrable Hw μ) (hHz : Integrable Hz μ)
    {S : Set X} (hS : MeasurableSet S)
    (hvz : (M.bilinear v z).restrict S=
      (signedSourceWeight (M.bilinear v w) χ+signedSourceWeight (M.bilinear v w) χ+
        (2 : ℝ) • μ.withDensityᵥ Hv).restrict S)
    (hwz : (M.bilinear w z).restrict S=
      (signedSourceWeight (M.bilinear w w) χ+signedSourceWeight (M.bilinear w w) χ+
        (2 : ℝ) • μ.withDensityᵥ Hw).restrict S)
    (hzz : (M.bilinear z z).restrict S=
      (signedSourceWeight (M.bilinear z w) χ+signedSourceWeight (M.bilinear z w) χ+
…

Mentions: OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.signedSourceWeight