pathELength_eq_lintegral_mfderiv_Ioo

English

Similarly, pathELength over an open interval Ioo(a,b) equals the lintegral of the mfderiv norm over that interval.

Русский

Аналогично, длина пути через открытый интервал Ioo(a,b) равна линтегралу нормы mfderiv по этому интервалу.

LaTeX

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

Lean4

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

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