Piecewise C¹ Curve API

General-purpose API for proving properties of piecewise C¹ curves by checking each consecutive segment defined by the partition.

Main results

• PiecewiseC1Curve.sortedPartition - the partition points as a sorted list
• PiecewiseC1Curve.consecutivePairs - consecutive pairs (pᵢ, pᵢ₊₁) from the sorted partition
• PiecewiseC1Curve.sortedPartition_head - the first element of the sorted partition is γ.a
• PiecewiseC1Curve.sortedPartition_last - the last element of the sorted partition is γ.b
• PiecewiseC1Curve.consecutivePairs_cover - union of [pᵢ, pᵢ₊₁] covers [a,b]
• PiecewiseC1Curve.forall_Icc_of_forall_consecutive - prove a property on [a,b] from each consecutive interval [pᵢ, pᵢ₊₁]

Definitions

noncomputable def PiecewiseC1Curve.sortedPartition (γ : PiecewiseC1Curve) : List ℝ

The sorted partition points as a list.

Equations

• γ.sortedPartition = γ.partition.sort fun (x1 x2 : ℝ) => x1 ≤ x2

noncomputable def PiecewiseC1Curve.consecutivePairs (γ : PiecewiseC1Curve) : List (ℝ × ℝ)

Consecutive pairs of partition points: [(p₀,p₁), (p₁,p₂), ...].

Equations

• γ.consecutivePairs = γ.sortedPartition.zip γ.sortedPartition.tail

Basic properties of sortedPartition

@[simp]

theorem PiecewiseC1Curve.mem_sortedPartition (γ : PiecewiseC1Curve) (x : ℝ) : x ∈ γ.sortedPartition ↔ x ∈ γ.partition

Membership in sortedPartition is equivalent to membership in the original partition.

theorem PiecewiseC1Curve.sortedPartition_sorted (γ : PiecewiseC1Curve) : List.Pairwise (fun (x1 x2 : ℝ) => x1 ≤ x2) γ.sortedPartition

The sortedPartition is sorted with respect to ≤.

theorem PiecewiseC1Curve.sortedPartition_nodup (γ : PiecewiseC1Curve) : γ.sortedPartition.Nodup

The sortedPartition has no duplicates.

theorem PiecewiseC1Curve.sortedPartition_nonempty (γ : PiecewiseC1Curve) : γ.sortedPartition ≠ []

The sortedPartition is nonempty (contains at least a and b).

theorem PiecewiseC1Curve.sortedPartition_mem_Icc (γ : PiecewiseC1Curve) (x : ℝ) (hx : x ∈ γ.sortedPartition) : x ∈ Set.Icc γ.a γ.b

Every element of the sortedPartition lies in [a, b].

Head and last of sortedPartition

theorem PiecewiseC1Curve.sortedPartition_head (γ : PiecewiseC1Curve) : γ.sortedPartition.head ⋯ = γ.a

The first element of the sorted partition equals γ.a.

Proof sketch: head ∈ [a,b] so a ≤ head; all elements ≥ head from sorted, and a ∈ sortedPartition, so head ≤ a. Together: head = a.

theorem PiecewiseC1Curve.sortedPartition_last (γ : PiecewiseC1Curve) : γ.sortedPartition.getLast ⋯ = γ.b

The last element of the sorted partition equals γ.b.

Proof sketch: getLast ∈ [a,b] so getLast ≤ b; all elements ≤ getLast from sorted, and b ∈ sortedPartition, so b ≤ getLast. Together: getLast = b.

Consecutive pairs cover [a, b]

theorem PiecewiseC1Curve.sortedPartition_tail_nonempty (γ : PiecewiseC1Curve) : γ.sortedPartition.tail ≠ []

The sorted partition has at least two elements (since a ≠ b are both in the partition).

theorem PiecewiseC1Curve.consecutivePairs_cover (γ : PiecewiseC1Curve) : Set.Icc γ.a γ.b ⊆ ⋃ p ∈ γ.consecutivePairs, Set.Icc p.1 p.2

The union of Icc p.1 p.2 over all p ∈ consecutivePairs γ covers [a, b].

Properties of consecutive pairs

theorem PiecewiseC1Curve.consecutivePairs_le (γ : PiecewiseC1Curve) (p : ℝ × ℝ) (hp : p ∈ γ.consecutivePairs) : p.1 ≤ p.2

For each consecutive pair (p, q), we have p ≤ q.

theorem PiecewiseC1Curve.consecutivePairs_subset (γ : PiecewiseC1Curve) (p : ℝ × ℝ) (hp : p ∈ γ.consecutivePairs) : p.1 ∈ Set.Icc γ.a γ.b ∧ p.2 ∈ Set.Icc γ.a γ.b

Both components of a consecutive pair lie in [a, b].

Main theorems

theorem PiecewiseC1Curve.forall_Icc_of_forall_consecutive {P : ℝ → Prop} (γ : PiecewiseC1Curve) (h : ∀ p ∈ γ.consecutivePairs, ∀ t ∈ Set.Icc p.1 p.2, P t) (t : ℝ) : t ∈ Set.Icc γ.a γ.b → P t

Main theorem: to prove a property P on [a, b], it suffices to prove P on each consecutive segment [pᵢ, pᵢ₊₁] of the partition.

theorem PiecewiseC1Curve.image_subset_of_consecutive_images {S : Set ℂ} (γ : PiecewiseC1Curve) (h : ∀ p ∈ γ.consecutivePairs, γ.toFun '' Set.Icc p.1 p.2 ⊆ S) : γ.toFun '' Set.Icc γ.a γ.b ⊆ S

Image variant: if the image of each consecutive segment lies in S, then the image of [a, b] lies in S.