AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementPositiveOperator

- A positive continuous-linear operator has a PSD matrix in every orthonormal basis. This is the coordinate bridge needed by the existing interior determinant theorem.

theorem toMatrix_posSemidef_of_isPositive
    (b : OrthonormalBasis ι ℝ E) (A : E →L[ℝ] E)
    (hA : A.IsPositive) :
    (LinearMap.toMatrix b.toBasis b.toBasis A.toLinearMap).PosSemidef := by
  exact (LinearMap.posSemidef_toMatrix_iff b).2 hA.toLinearMap

/-- Positive endpoint operator implies strict positivity of the interior
Jacobian determinant of the displacement derivative. -/

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementPositiveOperator.lean:44published source at 0e31a3cda412

- Positive endpoint operator implies strict positivity of the interior Jacobian determinant of the displacement derivative.

theorem det_affineDisplacementDerivative_pos_of_isPositive
    (b : OrthonormalBasis ι ℝ E) (A : E →L[ℝ] E)
    (hA : A.IsPositive)
    (t : ℝ) (ht0 : 0 ≤ t) (ht1 : t < 1) :
    0 < LinearMap.det (affineDisplacementDerivative A t).toLinearMap :=
  det_affineDisplacementDerivative_pos_of_posSemidef
    b.toBasis A (toMatrix_posSemidef_of_isPositive b A hA) t ht0 ht1

/-- The absolute Jacobian determinant is redundant at interior times when the
endpoint derivative is a positive operator. -/

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementPositiveOperator.lean:52published source at 0e31a3cda412

- The absolute Jacobian determinant is redundant at interior times when the endpoint derivative is a positive operator.

theorem abs_det_affineDisplacementDerivative_eq_of_isPositive
    (b : OrthonormalBasis ι ℝ E) (A : E →L[ℝ] E)
    (hA : A.IsPositive)
    (t : ℝ) (ht0 : 0 ≤ t) (ht1 : t < 1) :
    |LinearMap.det (affineDisplacementDerivative A t).toLinearMap| =
      LinearMap.det (affineDisplacementDerivative A t).toLinearMap :=
  abs_of_pos
    (det_affineDisplacementDerivative_pos_of_isPositive b A hA t ht0 ht1)

/-- Coordinate-free form of the interior displacement change-of-variables
join: the derivative hypothesis is stated as positivity of the operator, while
an orthonormal basis is used only internally to enter Mathlib's matrix PSD
interface. -/

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementPositiveOperator.lean:62published source at 0e31a3cda412

- Coordinate-free form of the interior displacement change-of-variables join: the derivative hypothesis is stated as positivity of the operator, while an orthonormal basis is used only internally to enter Mathlib's matrix PSD interface.

theorem integral_image_affineDisplacementMap_eq_integral_det_smul_of_isPositive
    (μ : Measure E) [MeasureTheory.Measure.IsAddHaarMeasure μ]
    (b : OrthonormalBasis ι ℝ E)
    {s : Set E} {T : E → E} {T' : E → E →L[ℝ] E}
    (hs : MeasurableSet s)
    (hderiv : ∀ x ∈ s, HasFDerivWithinAt T (T' x) s x)
    (hmono : IsMonotoneMap T)
    (hpos : ∀ x ∈ s, (T' x).IsPositive)
    (t : ℝ) (ht0 : 0 ≤ t) (ht1 : t < 1) (g : E → F) :
    ∫ y in affineDisplacementMap T t '' s, g y ∂μ =
      ∫ x in s,
        LinearMap.det
            (affineDisplacementDerivative (T' x) t).toLinearMap •
          g (affineDisplacementMap T t x) ∂μ := by
  exact integral_image_affineDisplacementMap_eq_integral_det_smul
    μ b.toBasis hs hderiv hmono
      (fun x hx => toMatrix_posSemidef_of_isPositive b (T' x) (hpos x hx))
      t ht0 ht1 g

end

end DisplacementPositiveOperator
end Measure
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementPositiveOperator.lean:75published source at 0e31a3cda412