ShiftedBochnerMeasure.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The full shifted Bochner measure

The trace inequality for the Hessian gives the displayed scalar lower bound. The associated positive quadratic measure is defined on pairs (function direction, scalar shift). In particular, the quadratic triangle inequality applies to two different Poisson replacements and retains all singular mass.

def OAI.RegularPointCoordinates.ShiftedBochnerLowerBound line 28
Source documentation
The scalar consequence of M >= |Hess f|² m and tr Hess f = Δf needed to subtract a constant multiple of the metric.
```
def ShiftedBochnerLowerBound (M : PositiveBilinearMeasure X E)
    (ν : Measure X) (ell : E →ₗ[ℝ] ℝ) (n : ℝ) : Prop :=
…
```
Mentions: OAI.RegularPointCoordinates.PositiveBilinearMeasure
def OAI.RegularPointCoordinates.shiftedBochnerMeasure line 35
Source documentation
Subtracting the trace correction from the full Bochner measure makes a positive bilinear measure on the augmented space.
```
def shiftedBochnerMeasure (M : PositiveBilinearMeasure X E)
    (ν : Measure X) [IsFiniteMeasure ν] (ell : E →ₗ[ℝ] ℝ) (n : ℝ)
    (h : ShiftedBochnerLowerBound M ν ell n) : PositiveBilinearMeasure X (WithLp 2 (E × ℝ)) where
…
```
Mentions: OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.ShiftedBochnerLowerBound
theorem OAI.RegularPointCoordinates.ShiftedBochnerMeasure.diagonal line 81
theorem OAI.RegularPointCoordinates.ShiftedBochnerMeasure.zero_shift line 89
Source documentation
The zero shift recovers the original measure, not just its density.
```
theorem zero_shift (v : E) :
    (shiftedBochnerMeasure M ν ell n h).measure (WithLp.toLp 2 (v, (0 : ℝ))) = M.measure v := by
…
```
Mentions: OAI.RegularPointCoordinates.shiftedBochnerMeasure
theorem OAI.RegularPointCoordinates.ShiftedBochnerMeasure.mass line 95

theorem OAI.RegularPointCoordinates.ShiftedBochnerMeasure.difference_mass_le line 106

Source documentation

The full-measure triangle estimate for two Poisson functions and two scalar metric shifts.

theorem difference_mass_le (v w : E) (b c : ℝ) (s : Set X) (hs : MeasurableSet s) :
    ((shiftedBochnerMeasure M ν ell n h).measure (WithLp.toLp 2 (v - w, b - c))).real s ≤
      2 * (((shiftedBochnerMeasure M ν ell n h).measure (WithLp.toLp 2 (v, b))).real s +
        ((shiftedBochnerMeasure M ν ell n h).measure (WithLp.toLp 2 (w, c))).real s) := by
…

Mentions: OAI.RegularPointCoordinates.shiftedBochnerMeasure

theorem OAI.RegularPointCoordinates.ShiftedBochnerMeasure.integral line 124

Source documentation

Bounded tests integrate the full shifted measure.

theorem integral (v : E) (b : ℝ) (χ : X →ᵇ ℝ) :
    (∫ x, χ x ∂(shiftedBochnerMeasure M ν ell n h).measure (WithLp.toLp 2 (v, b))) =
      (∫ x, χ x ∂M.measure v) - (2 * b * ell v - n * b ^ 2) * ∫ x, χ x ∂ν := by
…

Mentions: OAI.RegularPointCoordinates.shiftedBochnerMeasure