pathELength_eq_lintegral_mfderiv_Icc

English

For a path γ: Real → M and a,b real, pathELength equals the lintegral over Icc(a,b) of the ENorm of mfderiv along γ.

Русский

Для пути γ: ℝ → M и отрезка [a,b], длина пути равна лингенеральному интегралу по Icc(a,b) нормы mfderiv вдоль γ.

LaTeX

$$$$\\text{pathELength}(I,\\gamma,a,b)=\\int_{a}^{b} \\|\\mathrm{mfderiv}(I,\\gamma(t))\\|_e \\, dt.$$$$

Lean4

theorem pathELength_eq_lintegral_mfderiv_Icc : pathELength I γ a b = ∫⁻ t in Icc a b, ‖mfderiv 𝓘(ℝ) I γ t 1‖ₑ := by
  simp [pathELength]

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