OAI/Geometry/RCD/Sobolev/BochnerDensityShiftedQuadratic.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.bochner_measure_shifted_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_shifted_quadratic_bound (M : PositiveBilinearMeasure X (Euclidean m))
       (v w z : Euclidean m) (χ : X →ᵇ ℝ) (Hv Hw Hz s : X → ℝ)
       (D : X → Euclidean m →ₗ[ℝ] ℝ) (N b : ℝ) (hN : 0<N)
       (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=
   …

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