Connected-domain closure and separated branches

The closure argument only requires differentiability; derivatives need not vary continuously and zero values are treated by open level sets.

theorem PlanarMidpoint.is_const_of_isOpen_fiber {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] {s : Set E} {f : E → F} (hs : IsPreconnected s) (hf : ContinuousOn f s) {c : F} (hopen : IsOpen (s ∩ f ⁻¹' {c})) (hne : ∃ y ∈ s, f y = c) (x : E) : x ∈ s → f x = c

A nonempty open fiber of a continuous function on a preconnected set is the whole domain. The fiber is open in the ambient space.

theorem PlanarMidpoint.exists_is_const_of_fderiv_eq_zero_off_zero {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {s : Set E} {f : E → F} (hs : IsOpen s) (hconn : IsPreconnected s) (hf : DifferentiableOn ℝ f s) (hzero : ∀ x ∈ s, f x ≠ 0 → fderiv ℝ f x = 0) : ∃ (c : F), ∀ x ∈ s, f x = c

Derivative zero away from the zero fiber already forces constancy. This needs no continuity of the derivative and makes no assertion about passing derivatives across the boundary of the zero fiber.

theorem PlanarMidpoint.exists_is_const_of_regular_locus {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {s : Set E} {f : E → F} (hs : IsOpen s) (hconn : IsPreconnected s) (hf : DifferentiableOn ℝ f s) (G : Set F) (hG : IsOpen G) (hregular : ∀ x ∈ s, f x ∈ G → fderiv ℝ f x = 0) (hexceptional : (∀ x ∈ s, f x ∉ G) → ∀ x ∈ s, f x ≠ 0 → fderiv ℝ f x = 0) : ∃ (c : F), ∀ x ∈ s, f x = c

Two-stage closure for a differential rigidity argument. An attained value in an open regular locus propagates through a clopen fiber. If the regular locus is never attained, the exceptional-locus argument only needs to prove vanishing at nonzero values.

theorem PlanarMidpoint.eventually_eq_left_branch {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] {f g h : E → F} {x : E} (hf : ContinuousAt f x) (hh : ContinuousAt h x) (hsep : g x ≠ h x) (hfg : f x = g x) (hbranches : ∀ᶠ (y : E) in nhds x, f y = g y ∨ f y = h y) : f =ᶠ[nhds x] g

Two separated continuous branches cannot switch arbitrarily close to a point. The branch classification must hold throughout a neighborhood before this lemma can be used to identify derivatives.

theorem PlanarMidpoint.fderiv_eq_left_branch {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f g h : E → F} {x : E} (hf : ContinuousAt f x) (hh : ContinuousAt h x) (hsep : g x ≠ h x) (hfg : f x = g x) (hbranches : ∀ᶠ (y : E) in nhds x, f y = g y ∨ f y = h y) : fderiv ℝ f x = fderiv ℝ g x

Local equality with a selected branch identifies the full Fréchet derivative.