production module

`AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementMapInjectivity`

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

Imports

AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementMapDerivativeMathlib.Analysis.InnerProductSpace.Basic externalMathlib.Tactic external

Imported by

AutoSamplingTheory.TechnicalLemmas.MeasureAutoSamplingTheory.TechnicalLemmas.Measure.DisplacementChangeOfVariablesAutoSamplingTheory.TechnicalLemmas.Measure.DisplacementMonotoneDerivativeAutoSamplingTheory.TechnicalLemmas.Measure.DisplacementSupportingPotentialTests.DisplacementMapInjectivity

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

def AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementMapInjectivity.IsMonotoneMap Partial Not mapped

- Hilbert-space monotonicity of a point map.

def IsMonotoneMap (T : E → E) : Prop :=
  ∀ x y, 0 ≤ ⟪T x - T y, x - y⟫

/-- Exact inner-product expansion for the affine displacement map. -/

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementMapInjectivity.lean:36published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementMapInjectivity.inner_affineDisplacementMap_sub Partial Not mapped

- Exact inner-product expansion for the affine displacement map.

theorem inner_affineDisplacementMap_sub
    (T : E → E) (t : ℝ) (x y : E) :
    ⟪affineDisplacementMap T t x - affineDisplacementMap T t y, x - y⟫ =
      (1 - t) * ⟪x - y, x - y⟫ +
        t * ⟪T x - T y, x - y⟫ := by
  simp only [affineDisplacementMap, inner_sub_left, inner_add_left,
    real_inner_smul_left]
  ring

/-- Monotonicity of `T` gives a strong-monotonicity lower bound for the
interior displacement map. -/

AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementMapInjectivity.lean:40published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementMapInjectivity.affineDisplacementMap_inner_lower_bound Partial Not mapped

- Monotonicity of `T` gives a strong-monotonicity lower bound for the interior displacement map.

theorem affineDisplacementMap_inner_lower_bound
    {T : E → E} (hT : IsMonotoneMap T) (t : ℝ) (ht0 : 0 ≤ t)
    (x y : E) :
    (1 - t) * ‖x - y‖ ^ 2 ≤
      ⟪affineDisplacementMap T t x - affineDisplacementMap T t y, x - y⟫ := by
  rw [inner_affineDisplacementMap_sub]
  rw [inner_self_eq_norm_sq_to_K]
  exact le_add_of_nonneg_right (mul_nonneg ht0 (hT x y))

/-- For every `0 <= t < 1`, a monotone endpoint map produces an injective
interior displacement map. -/

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

theorem AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementMapInjectivity.injective_affineDisplacementMap_of_monotone Partial Not mapped

- For every `0 <= t < 1`, a monotone endpoint map produces an injective interior displacement map.

theorem injective_affineDisplacementMap_of_monotone
    {T : E → E} (hT : IsMonotoneMap T) (t : ℝ)
    (ht0 : 0 ≤ t) (ht1 : t < 1) :
    Function.Injective (affineDisplacementMap T t) := by
  intro x y hxy
  have hbound := affineDisplacementMap_inner_lower_bound hT t ht0 x y
  have hright :
      ⟪affineDisplacementMap T t x - affineDisplacementMap T t y, x - y⟫ = 0 := by
    rw [hxy]
    simp
  rw [hright] at hbound
  have hcoef : 0 < 1 - t := sub_pos.mpr ht1
  have hnorm_sq : ‖x - y‖ ^ 2 = 0 := by
    nlinarith [sq_nonneg ‖x - y‖]
  have hnorm : ‖x - y‖ = 0 := by
    nlinarith [norm_nonneg (x - y)]
  exact sub_eq_zero.mp (norm_eq_zero.mp hnorm)

end DisplacementMapInjectivity
end Measure
end TechnicalLemmas
end AutoSamplingTheory

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