production module

`AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementConvexGradientPositive`

3 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementConvexGradientPositive.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementConvexPotentialSupportAutoSamplingTheory.TechnicalLemmas.Measure.DisplacementGradientDerivativeSymmetryAutoSamplingTheory.TechnicalLemmas.Measure.DisplacementMonotoneDerivativeAutoSamplingTheory.TechnicalLemmas.Measure.DisplacementPositiveOperator

Imported by

AutoSamplingTheory.TechnicalLemmas.MeasureTests.DisplacementConvexGradientPositive

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

theorem AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementConvexGradientPositive.isPositive_fderiv_of_convex_gradient_field Partial Not mapped

- At every point where the gradient vector field of a globally convex potential is Frechet differentiable, its derivative is a positive operator. This statement is dimension-free.

theorem isPositive_fderiv_of_convex_gradient_field
    {phi : E → ℝ} {T : E → E} {A : E →L[ℝ] E} {x : E}
    (hconv : ConvexOn ℝ Set.univ phi)
    (hphi : ∀ y, HasFDerivAt phi (innerSL ℝ (T y)) y)
    (hT : HasFDerivAt T A x) :
    A.IsPositive := by
  have hmono : DisplacementMapInjectivity.IsMonotoneMap T :=
    DisplacementConvexPotentialSupport.isMonotoneMap_of_convexOn_univ_hasFDerivAt_inner
      hconv hphi
  have hsymm : A.IsSymmetric :=
    DisplacementGradientDerivativeSymmetry.isSymmetric_fderiv_of_gradient_field
      hphi hT
  exact
    DisplacementMonotoneDerivative.isPositive_fderiv_of_monotone_of_isSymmetric
      hmono hT hsymm

section FiniteDimensional

variable {ι : Type*}
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  [Fintype ι] [DecidableEq ι]

/-- In an orthonormal basis, the same local derivative therefore has a PSD
matrix representation.  The basis is only a coordinate witness; positivity is
proved before choosing it. -/

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementConvexGradientPositive.lean:39published source at 0e31a3cda412

theorem

AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementConvexGradientPositive.toMatrix_fderiv_posSemidef_of_convex_gradient_field

Partial Not mapped

- In an orthonormal basis, the same local derivative therefore has a PSD matrix representation. The basis is only a coordinate witness; positivity is proved before choosing it.

theorem toMatrix_fderiv_posSemidef_of_convex_gradient_field
    (b : OrthonormalBasis ι ℝ E)
    {phi : E → ℝ} {T : E → E} {A : E →L[ℝ] E} {x : E}
    (hconv : ConvexOn ℝ Set.univ phi)
    (hphi : ∀ y, HasFDerivAt phi (innerSL ℝ (T y)) y)
    (hT : HasFDerivAt T A x) :
    (LinearMap.toMatrix b.toBasis b.toBasis A.toLinearMap).PosSemidef :=
  DisplacementPositiveOperator.toMatrix_posSemidef_of_isPositive
    b A (isPositive_fderiv_of_convex_gradient_field hconv hphi hT)

/-- Consequently, the interior affine displacement derivative has strictly
positive determinant at every such differentiability point. -/

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementConvexGradientPositive.lean:65published source at 0e31a3cda412

theorem

AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementConvexGradientPositive.det_affineDisplacementDerivative_pos_of_convex_gradient_field

Partial Not mapped

- Consequently, the interior affine displacement derivative has strictly positive determinant at every such differentiability point.

theorem det_affineDisplacementDerivative_pos_of_convex_gradient_field
    (b : OrthonormalBasis ι ℝ E)
    {phi : E → ℝ} {T : E → E} {A : E →L[ℝ] E} {x : E}
    (hconv : ConvexOn ℝ Set.univ phi)
    (hphi : ∀ y, HasFDerivAt phi (innerSL ℝ (T y)) y)
    (hT : HasFDerivAt T A x)
    (t : ℝ) (ht0 : 0 ≤ t) (ht1 : t < 1) :
    0 < LinearMap.det
      (DisplacementMapDerivative.affineDisplacementDerivative A t).toLinearMap :=
  DisplacementPositiveOperator.det_affineDisplacementDerivative_pos_of_isPositive
    b A (isPositive_fderiv_of_convex_gradient_field hconv hphi hT) t ht0 ht1

end FiniteDimensional

end

end DisplacementConvexGradientPositive
end Measure
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementConvexGradientPositive.lean:77published source at 0e31a3cda412