intervalIntegrable_curveIntegralFun_trans_right

English

If ω and γbc are curve-integrable, then curveIntegralFun ω (γab.trans γbc) is interval-integrable on [1/2, 1], with a relation to γbc.

Русский

Если ω и γbc интегрируемы по кривой, то curveIntegralFun ω (γab.trans γbc) интегрируем на [1/2,1] и связано с γbc.

LaTeX

$$$ \\text{CurveIntegrable}(\\omega, γ_{bc}) \\Rightarrow \\operatorname{IntervalIntegrable}(\\curveIntegralFun(\\omega, γ_{ab}.trans γ_{bc}), \\mathrm{volume}, \\tfrac12, 1) $$$

Lean4

theorem intervalIntegrable_curveIntegralFun_trans_right (γab : Path a b) (h : CurveIntegrable ω γbc) :
    IntervalIntegrable (curveIntegralFun ω (γab.trans γbc)) volume (1 / 2) 1 :=
  by
  refine .congr_ae ?_ (curveIntegralFun_trans_aeeq_right _ _ _).symm
  simpa [ofNat_smul_eq_nsmul] using h.comp_sub_right 1 |>.comp_mul_left (c := 2) |>.smul (2 : 𝕜)

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