Segment differentiability for the homotopy

Proves that each segment of fdBoundaryToPolygonHomotopy is differentiable in t.

theorem RectHomotopyProof.fdBoundaryToPolygonHomotopy_seg1_differentiable (t _s : ℝ) : DifferentiableAt ℝ (fun (t' : ℝ) => 1 / 2 + (↑HHeight - ↑t' * (↑HHeight - ↑√3 / 2)) * Complex.I) t

Segment 1 formula (t < 1) is differentiable in t.

theorem RectHomotopyProof.fdBoundaryToPolygonHomotopy_seg4_differentiable (t _s : ℝ) : DifferentiableAt ℝ (fun (t' : ℝ) => -1 / 2 + (↑√3 / 2 + (↑t' - 3) * (↑HHeight - ↑√3 / 2)) * Complex.I) t

Segment 4 formula (3 < t ≤ 4) is differentiable in t.

theorem RectHomotopyProof.fdBoundaryToPolygonHomotopy_seg5_differentiable (t _s : ℝ) : DifferentiableAt ℝ (fun (t' : ℝ) => ↑t' - 9 / 2 + ↑HHeight * Complex.I) t

Segment 5 formula (t > 4) is differentiable in t.

theorem RectHomotopyProof.fdBoundaryToPolygonHomotopy_seg2_differentiable (t s : ℝ) : DifferentiableAt ℝ (fun (t' : ℝ) => have arc_point := Complex.exp ((↑Real.pi / 3 + (↑t' - 1) * (↑Real.pi / 2 - ↑Real.pi / 3)) * Complex.I); have chord_point := chordSegment rho' iPoint (t' - 1); (1 - s) • arc_point + s • chord_point) t

Segment 2 formula (1 < t ≤ 2) is differentiable in t.

theorem RectHomotopyProof.fdBoundaryToPolygonHomotopy_seg3_differentiable (t s : ℝ) : DifferentiableAt ℝ (fun (t' : ℝ) => have arc_point := Complex.exp ((↑Real.pi / 2 + (↑t' - 2) * (2 * ↑Real.pi / 3 - ↑Real.pi / 2)) * Complex.I); have chord_point := chordSegment iPoint rho (t' - 2); (1 - s) • arc_point + s • chord_point) t

Segment 3 formula (2 < t ≤ 3) is differentiable in t.