English
If ω is bounded by C on the segment [a,b], then the norm of the curve integral over the segment is at most C times the length of b−a.
Русский
Если ω ограничена на отрезке [a,b] выше C, то нормa интеграла по сегменту не превышает C·‖b−a‖.
LaTeX
$$$\\forall z \\in [a,b], \\|\\omega(z)\\| \\le C \\;\\Rightarrow\\; \\left\\| \\int_{\\text{segment}(a,b)} \\omega \\right\\| \\le C \\|b-a\\|$$$
Lean4
/-- If `‖ω z‖ ≤ C` at all points of the segment `[a -[ℝ] b]`,
then the curve integral `∫ᶜ x in .segment a b, ω x` has norm at most `C * ‖b - a‖`. -/
theorem norm_curveIntegral_segment_le [NormedSpace ℝ E] {C : ℝ} (h : ∀ z ∈ [a -[ℝ] b], ‖ω z‖ ≤ C) :
‖∫ᶜ x in .segment a b, ω x‖ ≤ C * ‖b - a‖ :=
calc
‖∫ᶜ x in .segment a b, ω x‖ ≤ C * ‖b - a‖ * |1 - 0| :=
by
letI : NormedSpace ℝ F := .restrictScalars ℝ 𝕜 F
rw [curveIntegral_segment]
refine intervalIntegral.norm_integral_le_of_norm_le_const fun t ht ↦ ?_
rw [segment_eq_image_lineMap] at h
rw [uIoc_of_le zero_le_one] at ht
apply_rules [(ω _).le_of_opNorm_le, mem_image_of_mem, Ioc_subset_Icc_self]
_ = C * ‖b - a‖ := by simp
