curveIntegralFun_trans_aeeq_right

English

Another restatement of the half-interval relation for concatenated paths with respect to the middle point.

Русский

Ещё одно разложение через середину для пути, полученного путём конкатенации.

LaTeX

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

Lean4

theorem curveIntegralFun_trans_aeeq_right (ω : E → E →L[𝕜] F) (γab : Path a b) (γbc : Path b c) :
    curveIntegralFun ω (γab.trans γbc) =ᵐ[volume.restrict (Ι (1 / 2 : ℝ) 1)] fun t ↦
      (2 : ℕ) • curveIntegralFun ω γbc (2 * t - 1) :=
  by
  rw [uIoc_of_le (by linarith), ← restrict_Ioo_eq_restrict_Ioc]
  filter_upwards [ae_restrict_mem measurableSet_Ioo] with t ⟨ht₁, ht₂⟩
  exact curveIntegralFun_trans_of_half_lt ω γab γbc ht₁

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