Polygon properties: values, segment functions, derivatives, differentiability

Defines per-segment functions fdPolygonSeg1..fdPolygonSeg5 and proves:

• Values at key points (fdPolygon_at_t1 .. fdPolygon_at_t4)
• Segment continuity and matching at breakpoints
• fdPolygon_continuous and fdPolygon_closed
• Derivative computation helpers and segment derivatives
• Segment differentiability and fdPolygon_differentiableAt_off_partition

theorem RectHomotopyProof.fdPolygon_at_t1 : fdPolygon 1 = rho'

theorem RectHomotopyProof.fdPolygon_at_t2 : fdPolygon 2 = iPoint

theorem RectHomotopyProof.fdPolygon_at_t3 : fdPolygon 3 = rho

theorem RectHomotopyProof.fdPolygon_at_t4 : fdPolygon 4 = -1 / 2 + ↑HHeight * Complex.I

noncomputable def RectHomotopyProof.fdPolygonSeg1 : ℝ → ℂ

The first segment of the boundary polygon (right vertical edge).

Equations

• RectHomotopyProof.fdPolygonSeg1 t = 1 / 2 + (↑RectHomotopyProof.HHeight - ↑t * (↑RectHomotopyProof.HHeight - ↑√3 / 2)) * Complex.I

noncomputable def RectHomotopyProof.fdPolygonSeg2 : ℝ → ℂ

The second segment of the boundary polygon (chord from ρ' to i).

Equations

• RectHomotopyProof.fdPolygonSeg2 t = RectHomotopyProof.chordSegment RectHomotopyProof.rho' RectHomotopyProof.iPoint (t - 1)

noncomputable def RectHomotopyProof.fdPolygonSeg3 : ℝ → ℂ

The third segment of the boundary polygon (chord from i to ρ).

Equations

• RectHomotopyProof.fdPolygonSeg3 t = RectHomotopyProof.chordSegment RectHomotopyProof.iPoint RectHomotopyProof.rho (t - 2)

noncomputable def RectHomotopyProof.fdPolygonSeg4 : ℝ → ℂ

The fourth segment of the boundary polygon (left vertical edge).

Equations

• RectHomotopyProof.fdPolygonSeg4 t = -1 / 2 + (↑√3 / 2 + (↑t - 3) * (↑RectHomotopyProof.HHeight - ↑√3 / 2)) * Complex.I

noncomputable def RectHomotopyProof.fdPolygonSeg5 : ℝ → ℂ

The fifth segment of the boundary polygon (top horizontal edge).

Equations

• RectHomotopyProof.fdPolygonSeg5 t = ↑t - 9 / 2 + ↑RectHomotopyProof.HHeight * Complex.I

theorem RectHomotopyProof.fdPolygon_seg1_continuous : Continuous fdPolygonSeg1

theorem RectHomotopyProof.fdPolygon_seg2_continuous : Continuous fdPolygonSeg2

theorem RectHomotopyProof.fdPolygon_seg3_continuous : Continuous fdPolygonSeg3

theorem RectHomotopyProof.fdPolygon_seg4_continuous : Continuous fdPolygonSeg4

theorem RectHomotopyProof.fdPolygon_seg5_continuous : Continuous fdPolygonSeg5

theorem RectHomotopyProof.fdPolygon_match_t1 : fdPolygonSeg1 1 = fdPolygonSeg2 1

theorem RectHomotopyProof.fdPolygon_match_t2 : fdPolygonSeg2 2 = fdPolygonSeg3 2

theorem RectHomotopyProof.fdPolygon_match_t3 : fdPolygonSeg3 3 = fdPolygonSeg4 3

theorem RectHomotopyProof.fdPolygon_match_t4 : fdPolygonSeg4 4 = fdPolygonSeg5 4

theorem RectHomotopyProof.fdPolygon_continuous : Continuous fdPolygon

theorem RectHomotopyProof.fdPolygon_closed : fdPolygon 0 = fdPolygon 5

theorem RectHomotopyProof.Complex.deriv_ofReal' : (deriv fun (t : ℝ) => ↑t) = fun (x : ℝ) => 1

theorem RectHomotopyProof.deriv_affine_mul (a b : ℂ) : (deriv fun (t : ℝ) => a + ↑t * b) = fun (x : ℝ) => b

theorem RectHomotopyProof.deriv_affine_shifted_mul (a b : ℂ) (c : ℝ) : (deriv fun (t : ℝ) => a + (↑t - ↑c) * b) = fun (x : ℝ) => b

theorem RectHomotopyProof.fdPolygon_deriv_seg1 : deriv fdPolygonSeg1 = fun (x : ℝ) => -(↑HHeight - ↑√3 / 2) * Complex.I

theorem RectHomotopyProof.fdPolygon_deriv_seg2 : deriv fdPolygonSeg2 = fun (x : ℝ) => iPoint - rho'

theorem RectHomotopyProof.fdPolygon_deriv_seg3 : deriv fdPolygonSeg3 = fun (x : ℝ) => rho - iPoint

theorem RectHomotopyProof.fdPolygon_deriv_seg4 : deriv fdPolygonSeg4 = fun (x : ℝ) => (↑HHeight - ↑√3 / 2) * Complex.I

theorem RectHomotopyProof.fdPolygon_deriv_seg5 : deriv fdPolygonSeg5 = fun (x : ℝ) => 1

theorem RectHomotopyProof.fdPolygon_seg1_differentiable : Differentiable ℝ fdPolygonSeg1

theorem RectHomotopyProof.fdPolygon_seg2_differentiable : Differentiable ℝ fdPolygonSeg2

theorem RectHomotopyProof.fdPolygon_seg3_differentiable : Differentiable ℝ fdPolygonSeg3

theorem RectHomotopyProof.fdPolygon_seg4_differentiable : Differentiable ℝ fdPolygonSeg4

theorem RectHomotopyProof.fdPolygon_seg5_differentiable : Differentiable ℝ fdPolygonSeg5

theorem RectHomotopyProof.fdPolygon_differentiableAt_off_partition (t : ℝ) (ht : t ∈ Set.Ioo 0 5) (ht_not_P : t ∉ {1, 2, 3, 4}) : DifferentiableAt ℝ fdPolygon t

theorem RectHomotopyProof.fdPolygon_seg1_deriv_val : -(↑HHeight - ↑√3 / 2) * Complex.I = -Complex.I

theorem RectHomotopyProof.fdPolygon_seg4_deriv_val : (↑HHeight - ↑√3 / 2) * Complex.I = Complex.I