English
For t with 1/2 < t, a corresponding relation with γbc holds, showing a dual formula when passing through the midpoint.
Русский
Для t, большего 1/2, выполняется соответствующая формула через γbc, демонстрирующая двойную форму через середину.
LaTeX
$$$ \\operatorname{curveIntegralFun}(\\omega, γ_{ab}.trans γ_{bc}, t) = (2) \\cdot \\operatorname{curveIntegralFun}(\\omega, γ_{bc}, 2t-1) $$$
Lean4
theorem curveIntegralFun_trans_of_lt_half (ω : E → E →L[𝕜] F) (γab : Path a b) (γbc : Path b c) (ht : t < 1 / 2) :
curveIntegralFun ω (γab.trans γbc) t = (2 : ℕ) • curveIntegralFun ω γab (2 * t) :=
by
let instE := NormedSpace.restrictScalars ℝ 𝕜 E
have H₁ : (γab.trans γbc).extend =ᶠ[𝓝 t] (fun s ↦ γab.extend (2 * s)) :=
(eventually_le_nhds ht).mono fun _ ↦ Path.extend_trans_of_le_half _ _
have H₂ : (2 : ℝ) • I =ᶠ[𝓝 (2 * t)] I :=
by
rw [LinearOrderedField.smul_Icc two_pos, mul_zero, mul_one, ← nhdsWithin_eq_iff_eventuallyEq]
rcases lt_trichotomy t 0 with ht₀ | rfl | ht₀
·
rw [notMem_closure_iff_nhdsWithin_eq_bot.mp, notMem_closure_iff_nhdsWithin_eq_bot.mp] <;> simp_intro h <;>
linarith
· simp
· rw [nhdsWithin_eq_nhds.2, nhdsWithin_eq_nhds.2] <;> simp [*] <;> linarith
rw [curveIntegralFun_def, H₁.self_of_nhds, H₁.derivWithin_eq_of_nhds, curveIntegralFun_def, derivWithin_comp_mul_left,
ofNat_smul_eq_nsmul, map_nsmul, derivWithin_congr_set H₂]
