WeightedBilinearMeasure.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Integrating full positive measure-valued forms

Bounded continuous weights act on the full signed measures. In particular, their singular parts contribute to every weighted quadratic form. These constructions do not assert existence of the local Bochner measure.

theorem OAI.RegularPointCoordinates.PositiveBilinearMeasure.integrable_weight line 28
def OAI.RegularPointCoordinates.PositiveBilinearMeasure.weightedBilinear line 38
Source documentation
Integration is bilinear in the coordinate directions, including the off-diagonal signed measures.
```
def weightedBilinear (w : X →ᵇ ℝ) : E →ₗ[ℝ] E →ₗ[ℝ] ℝ :=
…
```
def OAI.RegularPointCoordinates.PositiveBilinearMeasure.weightedContinuous line 53
def OAI.RegularPointCoordinates.PositiveBilinearMeasure.weightedOperator line 57
theorem OAI.RegularPointCoordinates.PositiveBilinearMeasure.weightedOperator_inner line 60
theorem OAI.RegularPointCoordinates.PositiveBilinearMeasure.measure_toSignedMeasure line 65
theorem OAI.RegularPointCoordinates.PositiveBilinearMeasure.weightedOperator_energy line 71
Source documentation
Diagonal weighted forms are ordinary integrals against the actual positive measure, without discarding singular mass.
```
theorem weightedOperator_energy (w : X →ᵇ ℝ) (v : E) :
    ⟪v, M.weightedOperator w v⟫_ℝ = ∫ x, w x ∂(M.measure v) := by
…
```
theorem OAI.RegularPointCoordinates.PositiveBilinearMeasure.weightedOperator_isSymmetric line 78
Source documentation
A real weighted measure-valued form stays symmetric even when the weight changes sign.
```
theorem weightedOperator_isSymmetric (w : X →ᵇ ℝ) :
    (M.weightedOperator w).IsSymmetric := by
…
```
theorem OAI.RegularPointCoordinates.PositiveBilinearMeasure.weightedOperator_isPositive line 88
theorem OAI.RegularPointCoordinates.PositiveBilinearMeasure.comap_weightedOperator line 104
Source documentation
A change of coordinates commutes with integration of full measures.
```
theorem comap_weightedOperator (A : E →L[ℝ] E) (w : X →ᵇ ℝ) :
    (M.comap A.toLinearMap).weightedOperator w =
      A.adjoint.comp ((M.weightedOperator w).comp A) := by
…
```
Mentions: OAI.RegularPointCoordinates.PositiveBilinearMeasure.weightedOperator
theorem OAI.RegularPointCoordinates.PositiveBilinearMeasure.weightedOperator_energy_mono line 115

theorem OAI.RegularPointCoordinates.PositiveBilinearMeasure.massOperator_le_weightedOperator line 127

Source documentation

A kernel lower bound controls the mass of every measurable testing set, including the singular part of the measure.

theorem massOperator_le_weightedOperator (w : X →ᵇ ℝ) (hw : ∀ x, 0 ≤ w x)
    (s : Set X) (hs : MeasurableSet s) (c : ℝ) (hc : ∀ x ∈ s, c ≤ w x) (v : E) :
    c * ⟪v, M.massOperator s v⟫_ℝ ≤ ⟪v, M.weightedOperator w v⟫_ℝ := by
…

theorem OAI.RegularPointCoordinates.PositiveBilinearMeasure.weightedOperator_le_massOperator line 142

Source documentation

A supported, bounded weight is bounded by the full mass on its support.

theorem weightedOperator_le_massOperator (w : X →ᵇ ℝ) (s : Set X)
    (hs : MeasurableSet s) (hws : ∀ x ∉ s, w x = 0) (C : ℝ)
    (hC : ∀ x ∈ s, w x ≤ C) (v : E) :
    ⟪v, M.weightedOperator w v⟫_ℝ ≤ C * ⟪v, M.massOperator s v⟫_ℝ := by
…

theorem OAI.RegularPointCoordinates.PositiveBilinearMeasure.weightedOperator_energy_difference_le line 159
Source documentation
A pointwise kernel-difference bound transfers to the full mass measure, without assuming that the measure has a density.
```
theorem weightedOperator_energy_difference_le (w z B : X →ᵇ ℝ)
    (hB : ∀ x, |w x - z x| ≤ B x) (v : E) :
    |⟪v, (M.weightedOperator w - M.weightedOperator z) v⟫_ℝ| ≤
      ⟪v, M.weightedOperator B v⟫_ℝ := by
…
```