pathELength_comp_of_antitoneOn — Mathlib

English

If f is monotone on Icc(a,b), differentiable, and MDifferentiable, then reparametrizing γ by f does not change the path length up to the interval mapping.

Русский

Если f монотонно на Icc(a,b), дифференцируема и MDifferentiable, то повторное параметрирование γ по f не изменяет длину траектории на соответствующем отрезке.

LaTeX

$$pathELength I (γ ∘ f) a b = pathELength I γ (f a) (f b)$$

Lean4

/-- The length of a path in a manifold is invariant under an antitone reparametrization. -/
theorem pathELength_comp_of_antitoneOn {f : ℝ → ℝ} (h : a ≤ b) (hf : AntitoneOn f (Icc a b))
    (h'f : DifferentiableOn ℝ f (Icc a b)) (hγ : MDifferentiableOn 𝓘(ℝ) I γ (Icc (f b) (f a))) :
    pathELength I (γ ∘ f) a b = pathELength I γ (f b) (f a) :=
  by
  rcases h.eq_or_lt with rfl | h
  · simp
  have f_im : f '' (Icc a b) = Icc (f b) (f a) := h'f.continuousOn.image_Icc_of_antitoneOn h.le hf
  simp only [pathELength_eq_lintegral_mfderivWithin_Icc, ← f_im]
  have B (t) (ht : t ∈ Icc a b) : HasDerivWithinAt f (derivWithin f (Icc a b) t) (Icc a b) t :=
    (h'f t ht).hasDerivWithinAt
  rw [lintegral_image_eq_lintegral_deriv_mul_of_antitoneOn measurableSet_Icc B hf]
  apply setLIntegral_congr_fun measurableSet_Icc (fun t ht ↦ ?_)
  have :
    (mfderivWithin 𝓘(ℝ, ℝ) I (γ ∘ f) (Icc a b) t) =
      (mfderivWithin 𝓘(ℝ, ℝ) I γ (Icc (f b) (f a)) (f t)) ∘L mfderivWithin 𝓘(ℝ) 𝓘(ℝ) f (Icc a b) t :=
    by
    rw [← f_im] at hγ ⊢
    apply mfderivWithin_comp
    · apply hγ _ (mem_image_of_mem _ ht)
    · rw [mdifferentiableWithinAt_iff_differentiableWithinAt]
      exact h'f _ ht
    · exact subset_preimage_image _ _
    · rw [uniqueMDiffWithinAt_iff_uniqueDiffWithinAt]
      exact uniqueDiffOn_Icc h _ ht
  rw [this]
  simp only [Function.comp_apply, ContinuousLinearMap.coe_comp']
  have : mfderivWithin 𝓘(ℝ) 𝓘(ℝ) f (Icc a b) t 1 = derivWithin f (Icc a b) t • (1 : TangentSpace 𝓘(ℝ) (f t)) :=
    by
    simp only [mfderivWithin_eq_fderivWithin, ← fderivWithin_derivWithin, smul_eq_mul, mul_one]
    rfl
  rw [this]
  have : 0 ≤ -derivWithin f (Icc a b) t := by simp [hf.derivWithin_nonpos]
  simp only [map_smul, enorm_smul, f_im, ← Real.enorm_of_nonneg this, enorm_neg]

Похожие утверждения