English
Composition with projection on Icc is equivalent to ContMDiff of f on Icc.
Русский
Композиция с проекцией на Icc эквивалентна ContMDiff функции на Icc.
LaTeX
$$$\ContMDiffOn (modelWithCornersSelf 𝕜 E) I n (f \circ (Set.projIcc x y h.out.le)) (Icc x y) w \iff \ContMDiff (𝓡∂ 1) I n f w$$$
Lean4
/-- The projection from `ℝ` to a closed segment is smooth on the segment, in the manifold sense. -/
theorem contMDiffOn_projIcc : ContMDiffOn 𝓘(ℝ) (𝓡∂ 1) n (Set.projIcc x y h.out.le) (Icc x y) :=
by
intro z hz
rw [contMDiffWithinAt_iff]
refine
⟨by apply ContinuousAt.continuousWithinAt; fun_prop, ?_⟩
-- We come back to the definition: we should check that, in each chart, the map is smooth
-- There are two charts, and we check things separately in each of them using the
-- explicit formulas.
suffices ContDiffWithinAt ℝ n _ (Icc x y) z by simpa
split_ifs with h'z
· have : ContDiff ℝ n (fun (w : ℝ) ↦ (show EuclideanSpace ℝ (Fin 1) from fun (_ : Fin 1) ↦ w - x)) :=
by
dsimp
apply contDiff_euclidean.2 (fun i ↦ by fun_prop)
apply this.contDiffWithinAt.congr_of_eventuallyEq_of_mem _ hz
filter_upwards [self_mem_nhdsWithin] with w hw
ext i
suffices max x (min y w) - x = w - x by simpa [modelWithCornersEuclideanHalfSpace, IccLeftChart]
rw [max_eq_right, min_eq_right hw.2]
simp [hw.1, h.out.le]
· have : ContDiff ℝ n (fun (w : ℝ) ↦ (show EuclideanSpace ℝ (Fin 1) from fun (_ : Fin 1) ↦ y - w)) :=
by
dsimp
apply contDiff_euclidean.2 (fun i ↦ by fun_prop)
apply this.contDiffWithinAt.congr_of_eventuallyEq_of_mem _ hz
filter_upwards [self_mem_nhdsWithin] with w hw
ext i
suffices y - max x (min y w) = y - w by simpa [modelWithCornersEuclideanHalfSpace, IccRightChart]
rw [max_eq_right, min_eq_right hw.2]
simp [hw.1, h.out.le]
