English
If a 1-form ω is continuous on a set s, and γ is a C^1-curve within s, then ω is curve-integrable along γ provided γ(t) ∈ s for all t.
Русский
Если 1-форма ω непрерывна на множестве s, и γ — путь класса C^1 внутри s, то ω интегрируема по кривой γ, если γ(t) ∈ s для всех t.
LaTeX
$$$\\text{ContinuousOn}(ω,s) \\to \\text{ContDiffOn}(\\mathbb{R},1, γ.extend I) \\to (∀ t, γ(t) ∈ s) \\Rightarrow \\text{CurveIntegrable}(ω, γ)$$$
Lean4
/-- If a 1-form `ω` is continuous on a set `s`,
then it is curve integrable along any $C^1$ path in this set. -/
theorem curveIntegrable_of_contDiffOn [NormedSpace ℝ E] {s : Set E} (hω : ContinuousOn ω s)
(hγ : ContDiffOn ℝ 1 γ.extend I) (hγs : ∀ t, γ t ∈ s) : CurveIntegrable ω γ :=
by
apply ContinuousOn.intervalIntegrable_of_Icc zero_le_one
simp only [funext (curveIntegralFun_def ω γ)]
apply ContinuousOn.clm_apply
· exact hω.comp (by fun_prop) fun _ _ ↦ hγs _
· exact hγ.continuousOn_derivWithin uniqueDiffOn_Icc_zero_one le_rfl
