Affine transport of smooth Jordan domains

Smooth strictly convex Jordan domains are stable under invertible real-linear maps and translations. Besides making the geometric package coordinate-free, this supplies ellipses as exact model domains: they are affine images of disks, with their transported boundary parametrizations and derivatives exposed by simp lemmas.

This file does not assert that ellipses approximate an arbitrary convex body. Its role is the reusable affine geometry needed by such approximation arguments.

theorem SmoothJordanDomain.deriv_continuousLinearEquiv_comp (Omega : SmoothJordanDomain) (e : ℂ ≃L[ℝ] ℂ) (t : ℝ) : deriv (⇑e ∘ Omega.boundaryParam) t = e (deriv Omega.boundaryParam t)

The derivative of a smooth Jordan parametrization after applying an invertible real-linear map.

noncomputable def SmoothJordanDomain.linearImage (Omega : SmoothJordanDomain) (e : ℂ ≃L[ℝ] ℂ) : SmoothJordanDomain

Transport a smooth Jordan domain by an invertible real-linear map.

Equations

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

@[simp]

theorem SmoothJordanDomain.linearImage_carrier (Omega : SmoothJordanDomain) (e : ℂ ≃L[ℝ] ℂ) : (Omega.linearImage e).carrier = ⇑e '' Omega.carrier

@[simp]

theorem SmoothJordanDomain.linearImage_boundaryParam (Omega : SmoothJordanDomain) (e : ℂ ≃L[ℝ] ℂ) : (Omega.linearImage e).boundaryParam = ⇑e ∘ Omega.boundaryParam

@[simp]

theorem SmoothJordanDomain.linearImage_boundaryParam_apply (Omega : SmoothJordanDomain) (e : ℂ ≃L[ℝ] ℂ) (t : ℝ) : (Omega.linearImage e).boundaryParam t = e (Omega.boundaryParam t)

theorem SmoothJordanDomain.linearImage_boundaryParam_deriv (Omega : SmoothJordanDomain) (e : ℂ ≃L[ℝ] ℂ) (t : ℝ) : deriv (Omega.linearImage e).boundaryParam t = e (deriv Omega.boundaryParam t)

theorem SmoothJordanDomain.deriv_const_add_boundaryParam (Omega : SmoothJordanDomain) (c : ℂ) (t : ℝ) : deriv (fun (u : ℝ) => c + Omega.boundaryParam u) t = deriv Omega.boundaryParam t

The derivative of a parametrization is unchanged by translation.

noncomputable def SmoothJordanDomain.translate (Omega : SmoothJordanDomain) (c : ℂ) : SmoothJordanDomain

Translate a smooth Jordan domain by a complex vector.

Equations

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

@[simp]

theorem SmoothJordanDomain.translate_carrier (Omega : SmoothJordanDomain) (c : ℂ) : (Omega.translate c).carrier = (fun (z : ℂ) => c + z) '' Omega.carrier

@[simp]

theorem SmoothJordanDomain.translate_boundaryParam (Omega : SmoothJordanDomain) (c : ℂ) : (Omega.translate c).boundaryParam = fun (t : ℝ) => c + Omega.boundaryParam t

@[simp]

theorem SmoothJordanDomain.translate_boundaryParam_apply (Omega : SmoothJordanDomain) (c : ℂ) (t : ℝ) : (Omega.translate c).boundaryParam t = c + Omega.boundaryParam t

theorem SmoothJordanDomain.translate_boundaryParam_deriv (Omega : SmoothJordanDomain) (c : ℂ) (t : ℝ) : deriv (Omega.translate c).boundaryParam t = deriv Omega.boundaryParam t

noncomputable def SmoothJordanDomain.ellipse (c : ℂ) (e : ℂ ≃L[ℝ] ℂ) (R : ℝ) (hR : 0 < R) : SmoothJordanDomain

An affine image of a positive-radius disk. In the real plane this is an ellipse, represented with its exact smooth regular boundary parametrization.

Equations

• SmoothJordanDomain.ellipse c e R hR = ((SmoothJordanDomain.ball 0 R hR).linearImage e).translate c

@[simp]

theorem SmoothJordanDomain.ellipse_carrier (c : ℂ) (e : ℂ ≃L[ℝ] ℂ) (R : ℝ) (hR : 0 < R) : (ellipse c e R hR).carrier = (fun (z : ℂ) => c + z) '' ⇑e '' Metric.ball 0 R

@[simp]

theorem SmoothJordanDomain.ellipse_boundaryParam (c : ℂ) (e : ℂ ≃L[ℝ] ℂ) (R : ℝ) (hR : 0 < R) : (ellipse c e R hR).boundaryParam = fun (t : ℝ) => c + e (circleMap 0 R t)

theorem SmoothJordanDomain.ellipse_boundaryParam_deriv (c : ℂ) (e : ℂ ≃L[ℝ] ℂ) (R : ℝ) (hR : 0 < R) (t : ℝ) : deriv (ellipse c e R hR).boundaryParam t = e (circleMap 0 R t * Complex.I)