production module

`AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementMapDerivative`

4 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementMapDerivative.lean.

Imports

Mathlib.Analysis.Calculus.FDeriv.Add external

Imported by

AutoSamplingTheory.TechnicalLemmas.MeasureAutoSamplingTheory.TechnicalLemmas.Measure.DisplacementDerivativeMatrixAutoSamplingTheory.TechnicalLemmas.Measure.DisplacementMapInjectivityTests.DisplacementMapDerivative

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

def AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementMapDerivative.affineDisplacementMap Partial Not mapped

- The point map whose pushforward gives displacement interpolation when an endpoint transport map `T` is available.

def affineDisplacementMap (T : E → E) (t : ℝ) : E → E :=
  fun x => (1 - t) • x + t • T x

/-- The affine continuous-linear map predicted by differentiating the
displacement point map. -/

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementMapDerivative.lean:33published source at 0e31a3cda412

def AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementMapDerivative.affineDisplacementDerivative Partial Not mapped

- The affine continuous-linear map predicted by differentiating the displacement point map.

def affineDisplacementDerivative (T' : E →L[ℝ] E) (t : ℝ) : E →L[ℝ] E :=
  (1 - t) • ContinuousLinearMap.id ℝ E + t • T'

/-- Pointwise Fréchet derivative of the displacement map. -/

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementMapDerivative.lean:38published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementMapDerivative.hasFDerivAt_affineDisplacementMap Partial Not mapped

- Pointwise Fréchet derivative of the displacement map.

theorem hasFDerivAt_affineDisplacementMap
    {T : E → E} {T' : E →L[ℝ] E} {x : E} (hT : HasFDerivAt T T' x)
    (t : ℝ) :
    HasFDerivAt (affineDisplacementMap T t)
      (affineDisplacementDerivative T' t) x := by
  change HasFDerivAt
    ((1 - t) • (id : E → E) + t • T)
    ((1 - t) • ContinuousLinearMap.id ℝ E + t • T') x
  exact ((hasFDerivAt_id x).const_smul (1 - t)).add (hT.const_smul t)

/-- Within-set Fréchet derivative in the form consumed by Mathlib's
change-of-variables API. -/

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementMapDerivative.lean:42published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementMapDerivative.hasFDerivWithinAt_affineDisplacementMap Partial Not mapped

- Within-set Fréchet derivative in the form consumed by Mathlib's change-of-variables API.

theorem hasFDerivWithinAt_affineDisplacementMap
    {T : E → E} {T' : E →L[ℝ] E} {s : Set E} {x : E}
    (hT : HasFDerivWithinAt T T' s x) (t : ℝ) :
    HasFDerivWithinAt (affineDisplacementMap T t)
      (affineDisplacementDerivative T' t) s x := by
  change HasFDerivWithinAt
    ((1 - t) • (id : E → E) + t • T)
    ((1 - t) • ContinuousLinearMap.id ℝ E + t • T') s x
  exact ((hasFDerivAt_id x).hasFDerivWithinAt.const_smul (1 - t)).add
    (hT.const_smul t)

end

end DisplacementMapDerivative
end Measure
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementMapDerivative.lean:54published source at 0e31a3cda412