production module

`AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementInterpolationCoupling`

5 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementInterpolationCoupling.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementInterpolation

Imported by

AutoSamplingTheory.TechnicalLemmas.MeasureAutoSamplingTheory.TechnicalLemmas.Measure.DisplacementInterpolationCostAutoSamplingTheory.TechnicalLemmas.Measure.DisplacementPotentialEnergyTests.DisplacementInterpolationCoupling

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

def AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementInterpolationCoupling.pointMap Partial Not mapped

- The affine point map used by displacement interpolation.

def pointMap (t : ℝ) : E × E → E :=
  fun z => (1 - t) • z.1 + t • z.2

@[fun_prop]

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementInterpolationCoupling.lean:28published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementInterpolationCoupling.measurable_pointMap Partial Not mapped

No declaration docstring.

theorem measurable_pointMap (t : ℝ) : Measurable (pointMap (E := E) t) := by
  unfold pointMap
  fun_prop

/-- Push the original endpoint coupling through the interpolation maps at two
times. -/

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementInterpolationCoupling.lean:32published source at 0e31a3cda412

def AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementInterpolationCoupling.interpolationCoupling Partial Not mapped

- Push the original endpoint coupling through the interpolation maps at two times.

noncomputable def interpolationCoupling
    (γ : Measure (E × E)) (s t : ℝ) : Measure (E × E) :=
  γ.map fun z => (pointMap (E := E) s z, pointMap (E := E) t z)

@[fun_prop]

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

theorem AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementInterpolationCoupling.measurable_pairPointMap Partial Not mapped

No declaration docstring.

theorem measurable_pairPointMap (s t : ℝ) :
    Measurable
      (fun z : E × E =>
        (pointMap (E := E) s z, pointMap (E := E) t z)) := by
  exact (measurable_pointMap s).prodMk (measurable_pointMap t)

/-- The two-time pushforward has the displacement law at time `s` as its first
marginal and the displacement law at time `t` as its second marginal. -/

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementInterpolationCoupling.lean:43published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementInterpolationCoupling.isCoupling_interpolationCoupling Partial Not mapped

- The two-time pushforward has the displacement law at time `s` as its first marginal and the displacement law at time `t` as its second marginal.

theorem isCoupling_interpolationCoupling
    (γ : Measure (E × E)) (s t : ℝ) :
    Transport.IsCoupling
      (interpolationCoupling γ s t)
      (DisplacementInterpolation.displacementInterpolation γ s)
      (DisplacementInterpolation.displacementInterpolation γ t) := by
  constructor
  · rw [Measure.fst, interpolationCoupling]
    rw [Measure.map_map measurable_fst (measurable_pairPointMap s t)]
    unfold DisplacementInterpolation.displacementInterpolation
    apply congrArg (fun f : E × E → E => Measure.map f γ)
    funext z
    rfl
  · rw [Measure.snd, interpolationCoupling]
    rw [Measure.map_map measurable_snd (measurable_pairPointMap s t)]
    unfold DisplacementInterpolation.displacementInterpolation
    apply congrArg (fun f : E × E → E => Measure.map f γ)
    funext z
    rfl

end

end DisplacementInterpolationCoupling
end Measure
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementInterpolationCoupling.lean:51published source at 0e31a3cda412