feat(Manifold/IntegralCurve/Transform): pointwise notation and translation lemmas for subtraction (leanprover-community#19008)

We restate the translation lemmas for integral curves using the `Pointwise` API and add translation lemmas for subtraction for convenience.

This is just split out from leanprover-community#9013.

The `Pointwise` API allows us to use lemmas like `Metric.vadd_ball` and more convenient rewriting of the `dt` term (rather than rewriting it inside the set builder notation).

Author: winstonyin

Mathlib/Geometry/Manifold/IntegralCurve/Transform.lean

@@ -20,7 +20,7 @@ curve.
 integral curve, vector field
 -/
 
-open Function Set
+open Function Set Pointwise
 
 variable
   {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
@@ -33,30 +33,35 @@ variable
 section Translation
 
 lemma IsIntegralCurveOn.comp_add (hγ : IsIntegralCurveOn γ v s) (dt : ℝ) :
-    IsIntegralCurveOn (γ ∘ (· + dt)) v { t | t + dt ∈ s } := by
+    IsIntegralCurveOn (γ ∘ (· + dt)) v (-dt +ᵥ s) := by
   intros t ht
   rw [comp_apply, ← ContinuousLinearMap.comp_id (ContinuousLinearMap.smulRight 1 (v (γ (t + dt))))]
+  rw [mem_vadd_set_iff_neg_vadd_mem, neg_neg, vadd_eq_add, add_comm,
+    ← mem_setOf (p := fun t ↦ t + dt ∈ s)] at ht
   apply HasMFDerivAt.comp t (hγ (t + dt) ht)
   refine ⟨(continuous_add_right _).continuousAt, ?_⟩
   simp only [mfld_simps, hasFDerivWithinAt_univ]
   exact HasFDerivAt.add_const (hasFDerivAt_id _) _
 
 lemma isIntegralCurveOn_comp_add {dt : ℝ} :
-    IsIntegralCurveOn γ v s ↔ IsIntegralCurveOn (γ ∘ (· + dt)) v { t | t + dt ∈ s } := by
+    IsIntegralCurveOn γ v s ↔ IsIntegralCurveOn (γ ∘ (· + dt)) v (-dt +ᵥ s) := by
   refine ⟨fun hγ ↦ hγ.comp_add _, fun hγ ↦ ?_⟩
   convert hγ.comp_add (-dt)
   · ext t
     simp only [Function.comp_apply, neg_add_cancel_right]
-  · simp only [mem_setOf_eq, neg_add_cancel_right, setOf_mem_eq]
+  · simp only [neg_neg, vadd_neg_vadd]
+
+lemma isIntegralCurveOn_comp_sub {dt : ℝ} :
+    IsIntegralCurveOn γ v s ↔ IsIntegralCurveOn (γ ∘ (· - dt)) v (dt +ᵥ s) := by
+  simpa using isIntegralCurveOn_comp_add (dt := -dt)
 
 lemma IsIntegralCurveAt.comp_add (hγ : IsIntegralCurveAt γ v t₀) (dt : ℝ) :
     IsIntegralCurveAt (γ ∘ (· + dt)) v (t₀ - dt) := by
   rw [isIntegralCurveAt_iff'] at *
   obtain ⟨ε, hε, h⟩ := hγ
   refine ⟨ε, hε, ?_⟩
   convert h.comp_add dt
-  ext t
-  rw [mem_setOf_eq, Metric.mem_ball, Metric.mem_ball, dist_sub_eq_dist_add_right]
+  rw [Metric.vadd_ball, vadd_eq_add, neg_add_eq_sub]
 
 lemma isIntegralCurveAt_comp_add {dt : ℝ} :
     IsIntegralCurveAt γ v t₀ ↔ IsIntegralCurveAt (γ ∘ (· + dt)) v (t₀ - dt) := by
@@ -66,10 +71,14 @@ lemma isIntegralCurveAt_comp_add {dt : ℝ} :
     simp only [Function.comp_apply, neg_add_cancel_right]
   · simp only [sub_neg_eq_add, sub_add_cancel]
 
+lemma isIntegralCurveAt_comp_sub {dt : ℝ} :
+    IsIntegralCurveAt γ v t₀ ↔ IsIntegralCurveAt (γ ∘ (· - dt)) v (t₀ + dt) := by
+  simpa using isIntegralCurveAt_comp_add (dt := -dt)
+
 lemma IsIntegralCurve.comp_add (hγ : IsIntegralCurve γ v) (dt : ℝ) :
     IsIntegralCurve (γ ∘ (· + dt)) v := by
   rw [isIntegralCurve_iff_isIntegralCurveOn] at *
-  exact hγ.comp_add _
+  simpa using hγ.comp_add dt
 
 lemma isIntegralCurve_comp_add {dt : ℝ} :
     IsIntegralCurve γ v ↔ IsIntegralCurve (γ ∘ (· + dt)) v := by
@@ -78,6 +87,10 @@ lemma isIntegralCurve_comp_add {dt : ℝ} :
   ext t
   simp only [Function.comp_apply, neg_add_cancel_right]
 
+lemma isIntegralCurve_comp_sub {dt : ℝ} :
+    IsIntegralCurve γ v ↔ IsIntegralCurve (γ ∘ (· - dt)) v := by
+  simpa using isIntegralCurve_comp_add (dt := -dt)
+
 end Translation
 
 /-! ### Scaling lemmas -/