intervalIntegrable_curveIntegralFun_trans_left

English

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

Русский

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

LaTeX

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

Lean4

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

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