PositiveBilinearMeasure.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Positive measure-valued forms on a finite coordinate span

This constructs the real mass operators from a finite family of signed measures, retaining singular mass. The existence and local Bochner identification of that family are separate analytic obligations.

structure OAI.RegularPointCoordinates.PositiveBilinearMeasure line 24
Source documentation
The finite-dimensional restriction of a positive, symmetric, measure-valued quadratic form, such as the local Bochner measure.
```
structure PositiveBilinearMeasure (X E : Type*) [MeasurableSpace X]
    [AddCommGroup E] [Module ℝ E] where
…
```
def OAI.RegularPointCoordinates.PositiveBilinearMeasure.evaluated line 36
def OAI.RegularPointCoordinates.PositiveBilinearMeasure.evaluatedContinuous line 43
def OAI.RegularPointCoordinates.PositiveBilinearMeasure.massOperator line 47
theorem OAI.RegularPointCoordinates.PositiveBilinearMeasure.massOperator_inner line 50
theorem OAI.RegularPointCoordinates.PositiveBilinearMeasure.massOperator_isPositive line 54
def OAI.RegularPointCoordinates.PositiveBilinearMeasure.measure line 71
Source documentation
Every diagonal signed measure is converted to an actual positive finite measure, rather than replaced by a density with respect to volume.
```
def measure (v : E) : Measure X :=
…
```
instance OAI.RegularPointCoordinates.PositiveBilinearMeasure.measure_finite line 75
theorem OAI.RegularPointCoordinates.PositiveBilinearMeasure.measure_real line 78
def OAI.RegularPointCoordinates.PositiveBilinearMeasure.comap line 88
Source documentation
Change of coordinate columns acts on the full signed measures.
```
def comap (A : E →ₗ[ℝ] E) : PositiveBilinearMeasure X E where
…
```
Mentions: OAI.RegularPointCoordinates.PositiveBilinearMeasure
theorem OAI.RegularPointCoordinates.PositiveBilinearMeasure.comap_massOperator line 93
theorem OAI.RegularPointCoordinates.PositiveBilinearMeasure.measure_add_le line 106
Source documentation
The quadratic triangle bound holds for the full measure on every measurable set, so singular mass is included.
```
theorem measure_add_le (v w : E) (s : Set X) (hs : MeasurableSet s) :
    (M.measure (v + w)).real s ≤ 2 * ((M.measure v).real s + (M.measure w).real s) := by
…
```
theorem OAI.RegularPointCoordinates.PositiveBilinearMeasure.comap_measure_real line 118
Source documentation
Covariance for the actual positive diagonal measures.
```
theorem comap_measure_real (A : E →L[ℝ] E) (v : E) (s : Set X)
    (hs : MeasurableSet s) :
    ((M.comap A.toLinearMap).measure v).real s = (M.measure (A v)).real s := by
…
```
Mentions: OAI.RegularPointCoordinates.PositiveBilinearMeasure.measure
def OAI.RegularPointCoordinates.PositiveBilinearMeasure.traceMass line 129
theorem OAI.RegularPointCoordinates.PositiveBilinearMeasure.traceMass_nonneg line 132

theorem OAI.RegularPointCoordinates.PositiveBilinearMeasure.mass_entry_le_trace line 136

Source documentation

Positivity bounds every matrix entry by its trace.

theorem mass_entry_le_trace (s : Set X) (hs : MeasurableSet s) (i j : Fin n) :
    |N.massOperator s (EuclideanSpace.single j 1) i| ≤ N.traceMass s := by
…

theorem OAI.RegularPointCoordinates.PositiveBilinearMeasure.massOperator_norm_le_trace line 165