curveIntegralFun_trans_of_half_lt

English

A variant of the half-interval law giving another equivalent expression for the concatenated path in terms of the second segment.

Русский

Вариант закона через середину, дающий эквивалентное выражение для объединённого пути через вторую часть.

LaTeX

$$$ \\operatorname{curveIntegralFun}(\\omega, γ_{ab}.trans γ_{bc}, t) = 2 \\cdot \\operatorname{curveIntegralFun}(\\omega, γ_{bc}, 2t-1) $ for t in appropriate interval$$

Lean4

theorem curveIntegralFun_trans_of_half_lt (ω : E → E →L[𝕜] F) (γab : Path a b) (γbc : Path b c) (ht₀ : 1 / 2 < t) :
    curveIntegralFun ω (γab.trans γbc) t = (2 : ℕ) • curveIntegralFun ω γbc (2 * t - 1) :=
  by
  rw [← (γab.trans γbc).symm_symm, curveIntegralFun_symm_apply, Path.trans_symm,
    curveIntegralFun_trans_of_lt_half (ht := by linarith), curveIntegralFun_symm_apply, smul_neg, neg_neg]
  congr 2
  ring

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