continuousOn_comp_compProj — Mathlib

English

If hf is IsPicardLindelöf and α is in FunSpace, then t ↦ f(t, α.compProj t) is interval-integrable on t0..t.

Русский

Если hf — IsPicardLindelöf и α ∈ FunSpace, то функция t ↦ f(t, α.compProj t) интегрируема на отрезке t0..t.

LaTeX

$$IntervalIntegrable (fun t' => f t' (α.compProj t')) volume t0 t$$

Lean4

/-- The integrand in `next` is continuous. -/
theorem continuousOn_comp_compProj (hf : IsPicardLindelof f t₀ x₀ a r L K) (α : FunSpace t₀ x₀ r L) :
    ContinuousOn (fun t' ↦ f t' (α.compProj t')) (Icc tmin tmax) :=
  continuousOn_comp
    (continuousOn_prod_of_continuousOn_lipschitzOnWith' (uncurry f) K hf.lipschitzOnWith hf.continuousOn)
    α.continuous_compProj.continuousOn fun _ _ ↦ α.mem_closedBall hf.mul_max_le

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