Fundamental Domain Boundary – Smoothness

Differentiability, derivatives, limits, and curve/immersion constructions for the fundamental domain boundary.

Main Definitions

• fdBoundaryHCurve — H-parameterized boundary as PiecewiseC1Curve
• fdBoundaryHImmersion — H-parameterized boundary as PiecewiseC1Immersion
• fdBoundaryCurve — fixed-height boundary as PiecewiseC1Curve
• fdBoundaryImmersion — fixed-height boundary as PiecewiseC1Immersion

theorem fdBoundary_H_differentiableAt_off_partition (H t : ℝ) (htp : t ∉ fdBoundaryHPartition) : DifferentiableAt ℝ (fdBoundaryH H) t

theorem fdBoundary_H_hasDerivAt_seg1' (H t : ℝ) (ht : t ∈ Set.Ioo 0 1) : HasDerivAt (fdBoundaryH H) (-(↑H - ↑√3 / 2) * Complex.I) t

theorem fdBoundary_H_hasDerivAt_seg4' (H t : ℝ) (ht : t ∈ Set.Ioo 3 4) : HasDerivAt (fdBoundaryH H) ((↑H - ↑√3 / 2) * Complex.I) t

theorem fdBoundary_H_hasDerivAt_seg5' (H t : ℝ) (ht : t ∈ Set.Ioo 4 5) : HasDerivAt (fdBoundaryH H) 1 t

theorem fdBoundary_H_deriv_ne_zero_off_fullPartition (H : ℝ) (hH : √3 / 2 < H) (t : ℝ) (ht : t ∈ Set.Icc 0 5) (htp : t ∉ fdBoundaryFullPartition) : deriv (fdBoundaryH H) t ≠ 0

theorem fdBoundary_H_deriv_continuousAt_off_fullPartition (H t : ℝ) (ht : t ∈ Set.Ioo 0 5) (htp : t ∉ fdBoundaryFullPartition) : ContinuousAt (deriv (fdBoundaryH H)) t

theorem fdBoundary_H_left_deriv_limit (H : ℝ) (hH : √3 / 2 < H) (p : ℝ) (hp : p ∈ fdBoundaryFullPartition) (hp' : 0 < p) : ∃ (L : ℂ), L ≠ 0 ∧ Filter.Tendsto (deriv (fdBoundaryH H)) (nhdsWithin p (Set.Iio p)) (nhds L)

theorem fdBoundary_H_hasDerivAt_seg1 (H : ℝ) {t : ℝ} (ht : t < 1) : HasDerivAt (fdBoundaryH H) (-(↑H - ↑√3 / 2) * Complex.I) t

theorem fdBoundary_H_hasDerivAt_seg4 (H : ℝ) {t : ℝ} (h3 : 3 < t) (h4 : t < 4) : HasDerivAt (fdBoundaryH H) ((↑H - ↑√3 / 2) * Complex.I) t

theorem fdBoundary_H_hasDerivAt_seg5 (H : ℝ) {t : ℝ} (h4 : 4 < t) : HasDerivAt (fdBoundaryH H) 1 t

theorem continuous_fdBoundary_seg1_H (H : ℝ) : Continuous (fdBoundarySeg1H H)

theorem continuous_fdBoundary_seg4_H (H : ℝ) : Continuous (fdBoundarySeg4H H)

theorem continuous_fdBoundary_seg5_H (H : ℝ) : Continuous (fdBoundarySeg5H H)

theorem hasDerivAt_fdBoundary_seg1_H (H t : ℝ) : HasDerivAt (fdBoundarySeg1H H) (-↑(H - √3 / 2) * Complex.I) t

theorem hasDerivAt_fdBoundary_seg4_H (H t : ℝ) : HasDerivAt (fdBoundarySeg4H H) (↑(H - √3 / 2) * Complex.I) t

theorem hasDerivAt_fdBoundary_seg5_H (H t : ℝ) : HasDerivAt (fdBoundarySeg5H H) 1 t

theorem fdBoundary_H_not_differentiableAt_4 {H : ℝ} (hH : √3 / 2 < H) : ¬DifferentiableAt ℝ (fdBoundaryH H) 4

theorem fdBoundary_H_not_differentiableAt_3 {H : ℝ} (_hH : √3 / 2 < H) : ¬DifferentiableAt ℝ (fdBoundaryH H) 3

theorem fdBoundary_H_not_differentiableAt_1 {H : ℝ} (_hH : √3 / 2 < H) : ¬DifferentiableAt ℝ (fdBoundaryH H) 1

theorem fdBoundary_H_right_deriv_limit (H : ℝ) (hH : √3 / 2 < H) (p : ℝ) (hp : p ∈ fdBoundaryFullPartition) (hp' : p < 5) : ∃ (L : ℂ), L ≠ 0 ∧ Filter.Tendsto (deriv (fdBoundaryH H)) (nhdsWithin p (Set.Ioi p)) (nhds L)

noncomputable def fdBoundaryHCurve (H : ℝ) : PiecewiseC1Curve

The H-parameterized boundary as a PiecewiseC1Curve.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def fdBoundaryHImmersion (H : ℝ) (hH : √3 / 2 < H) : PiecewiseC1Immersion

The H-parameterized boundary as a PiecewiseC1Immersion. Requires H > √3/2 for nonzero derivative.

Equations

• fdBoundaryHImmersion H hH = { toPiecewiseC1Curve := fdBoundaryHCurve H, deriv_ne_zero := ⋯, left_deriv_limit := ⋯, right_deriv_limit := ⋯ }

theorem fdBoundary_HCurve_closed (H : ℝ) : (fdBoundaryHCurve H).IsClosed

theorem fdBoundary_differentiableAt_off_partition (t : ℝ) (htp : t ∉ fdPartition) : DifferentiableAt ℝ fdBoundary t

theorem fdBoundary_deriv_continuousAt_off_partition (t : ℝ) (ht : t ∈ Set.Ioo 0 5) (htp : t ∉ fdBoundaryFullPartition) : ContinuousAt (deriv fdBoundary) t

theorem fdBoundary_deriv_ne_zero_off_partition (t : ℝ) (ht : t ∈ Set.Icc 0 5) (htp : t ∉ fdBoundaryFullPartition) : deriv fdBoundary t ≠ 0

theorem fdBoundary_left_deriv_limit (p : ℝ) (hp : p ∈ fdBoundaryFullPartition) (hp' : 0 < p) : ∃ (L : ℂ), L ≠ 0 ∧ Filter.Tendsto (deriv fdBoundary) (nhdsWithin p (Set.Iio p)) (nhds L)

theorem fdBoundary_right_deriv_limit (p : ℝ) (hp : p ∈ fdBoundaryFullPartition) (hp' : p < 5) : ∃ (L : ℂ), L ≠ 0 ∧ Filter.Tendsto (deriv fdBoundary) (nhdsWithin p (Set.Ioi p)) (nhds L)

noncomputable def fdBoundaryCurve : PiecewiseC1Curve

The boundary of the fundamental domain as a PiecewiseC1Curve.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def fdBoundaryImmersion : PiecewiseC1Immersion

The boundary of the fundamental domain as a PiecewiseC1Immersion.

Equations

• fdBoundaryImmersion = { toPiecewiseC1Curve := fdBoundaryCurve, deriv_ne_zero := ⋯, left_deriv_limit := ⋯, right_deriv_limit := ⋯ }

theorem fdBoundaryImmersion_closed : fdBoundaryCurve.IsClosed

theorem fdBoundary_H_hasDerivAt_arc (H : ℝ) {t : ℝ} (h1 : 1 < t) (h3 : t < 3) : HasDerivAt (fdBoundaryH H) (Complex.exp (↑Real.pi * (↑t + 1) / 6 * Complex.I) * (↑Real.pi / 6 * Complex.I)) t

theorem fdBoundary_H_deriv_continuousOn_Ioo_01 (H : ℝ) : ContinuousOn (deriv (fdBoundaryH H)) (Set.Ioo 0 1)

theorem fdBoundary_H_deriv_continuousOn_Ioo_13 (H : ℝ) : ContinuousOn (deriv (fdBoundaryH H)) (Set.Ioo 1 3)

theorem fdBoundary_H_deriv_continuousOn_Ioo_34 (H : ℝ) : ContinuousOn (deriv (fdBoundaryH H)) (Set.Ioo 3 4)

theorem fdBoundary_H_deriv_continuousOn_Ioo_45 (H : ℝ) : ContinuousOn (deriv (fdBoundaryH H)) (Set.Ioo 4 5)

theorem fdBoundary_H_deriv_bound_ex {H : ℝ} (hH : √3 / 2 < H) : ∃ (M : ℝ), 0 < M ∧ ∀ t ∉ fdBoundaryHPartition, ‖deriv (fdBoundaryH H) t‖ ≤ M

theorem fdBoundary_H_deriv_continuousOn_off_partition (H : ℝ) : ContinuousOn (deriv (fdBoundaryH H)) (Set.Icc 0 5 \ ↑fdBoundaryHPartition)