Domains with Lipschitz boundary

Set.IsLipschitzChart is the shared uncentred geometric chart in an arbitrary real normed ambient space. Set.IsLipschitzChartWith adds normalization of its graph at zero, as required by the Sobolev consumers. Set.IsLipschitzDomain allows the bound to vary along the frontier; Set.IsLipschitzDomainWith retains its distinct uniform quantitative bound. The theorem Set.isLipschitzDomain_iff_forall_exists_isLipschitzDomainAtWith relates these conditions.

Charts can be recentred and transported by affine isometries or positive dilation. Domains with compact frontier have finite chart covers with a common bound; epigraphs of globally Lipschitz functions are examples.

A shared chart identifies a set in a real normed ambient space with an epigraph inside a cylinder in the real normed model space WithLp 2 (ℝ × E). The centered predicate Set.IsLipschitzChartWith additionally requires that the graph pass through the chart centre. For centered charts the normal and tangential radii can be reduced without changing the coordinates or the graph. Shared charts have no normalization requirement on the graph.

The global predicate Set.IsLipschitzDomainWith requires a chart centred at every frontier point, with a single Lipschitz bound for all local graphs. It is invariant under affine isometries and positive dilations, and on a compact part of the frontier finitely many charts suffice. These are the geometric hypotheses used to transport Sobolev trace and extension operators from a flat half-space through boundary charts and to patch them with a partition of unity.

Locally Lipschitz boundary graphs extend to global graphs with the same constant and radii, using Mathlib's LipschitzOnWith.extend_real. The open set TauCeti.chartEpigraph and its support-containment lemmas provide the shared geometry for chart trace and extension operators.

Main declarations

• TauCeti.normalCylinder: the product cylinder used by boundary charts.
• Set.isLipschitzChart_of_forall_mem_iff: a chart whose cylinder meets a set exactly above a Lipschitz graph is a Lipschitz boundary chart.
• Set.IsLipschitzChartWith: a Lipschitz boundary chart with given coordinates, graph and radii.
• Set.IsLipschitzDomainAtWith: the existence of a Lipschitz boundary chart centred at one point.
• Set.IsLipschitzDomainWith: an open set with the local graph condition at every frontier point.
• Set.IsLipschitzChartWith.lipschitzWith, Set.IsLipschitzChartWith.apply_zero: the graph of a chart is L-Lipschitz and passes through the centre.
• TauCeti.exists_isLipschitzChartWith_of_lipschitzOnWith: extension of a local Lipschitz graph to a global graph defining the same boundary chart.
• Set.IsLipschitzChartWith.mono_radii: restriction of a chart to a smaller cylinder.
• Set.IsLipschitzChartWith.exists_mono_radii_two_mul_lt: restriction to a cylinder whose normal radius exceeds twice the graph's tangential rise.
• Set.IsLipschitzChartWith.smul: positive dilation of a chart, with explicit coordinates TauCeti.dilateConj, graph and radii.
• Set.IsLipschitzDomainWith.smul: positive dilations preserve Lipschitz domains and constants.
• Set.isLipschitzDomainWith_image_iff: the image of a set Ω ⊆ F under an affine isometry onto the model space is a Lipschitz domain exactly when Ω is open with a chart at every frontier point.
• Set.IsLipschitzDomainWith.exists_finset_isLipschitzChartWith_cover: the frontier of a bounded Lipschitz domain is covered by finitely many chart cylinders with a common Lipschitz constant.
• Set.IsLipschitzDomainWith.exists_finset_isLipschitzChartWith_two_mul_lt_cover: the frontier of a bounded Lipschitz domain is covered by finitely many shortened chart cylinders.
• Set.IsLipschitzDomain.exists_isLipschitzDomainWith: a Lipschitz domain with compact frontier has a uniform Lipschitz bound.

References

• L. C. Evans, Partial Differential Equations, 2nd ed., §5.5.
• W. McLean, Strongly Elliptic Systems and Boundary Integral Equations, §3.1.
• P. Grisvard, Elliptic Problems in Nonsmooth Domains, Definition 1.2.1.1.
• L. C. Evans and R. F. Gariepy, Measure Theory and Fine Properties of Functions, §4.3.

def TauCeti.normalCylinder {E : Type u_1} [SeminormedAddCommGroup E] (a b : ℝ) : Set (WithLp 2 (ℝ × E))

The open product cylinder of normal radius a and tangential radius b, centred at the origin of WithLp 2 (ℝ × E).

@[simp]

theorem TauCeti.mem_normalCylinder {E : Type u_1} [SeminormedAddCommGroup E] {a b : ℝ} {x : WithLp 2 (ℝ × E)} : x ∈ normalCylinder a b ↔ -a < x.fst ∧ x.fst < a ∧ ‖x.snd‖ < b

Membership in the normal product cylinder, in terms of its two coordinates.

theorem TauCeti.isOpen_normalCylinder {E : Type u_1} [SeminormedAddCommGroup E] (a b : ℝ) : IsOpen (normalCylinder a b)

A normal product cylinder is open.

theorem TauCeti.isBounded_normalCylinder {E : Type u_1} [SeminormedAddCommGroup E] (a b : ℝ) : Bornology.IsBounded (normalCylinder a b)

A normal product cylinder is bounded.

theorem TauCeti.normalCylinder_mono {E : Type u_1} [SeminormedAddCommGroup E] {a b a' b' : ℝ} (ha : a' ≤ a) (hb : b' ≤ b) : normalCylinder a' b' ⊆ normalCylinder a b

Shrinking either radius shrinks the normal product cylinder.

theorem TauCeti.zero_mem_normalCylinder {E : Type u_1} [SeminormedAddCommGroup E] {a b : ℝ} (ha : 0 < a) (hb : 0 < b) : 0 ∈ normalCylinder a b

A normal product cylinder with positive radii contains its centre.

theorem TauCeti.smul_normalCylinder {E : Type u_1} [SeminormedAddCommGroup E] [MulAction ℝ E] [NormSMulClass ℝ E] {c : ℝ} (hc : 0 < c) (a b : ℝ) : c • normalCylinder a b = normalCylinder (c * a) (c * b)

Dilating a normal product cylinder by c > 0 multiplies both radii by c.

Lipschitz boundary charts

structure Set.IsLipschitzChart {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (Ω : Set F) (e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)) (γ : E → ℝ) (K : NNReal) (h r : ℝ) : Prop

A Lipschitz boundary chart of Ω ⊆ F. In the coordinates given by the affine isometry e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E), the part of Ω inside the open cylinder normalCylinder h r is the part of that cylinder strictly above the graph x.fst = γ x.snd of the K-Lipschitz function γ : E → ℝ.

• height_pos : 0 < h

  The cylinder has positive half-height.

• radius_pos : 0 < r

  The cylinder has positive radius.

• lipschitzWith : LipschitzWith K γ

  The graph function is K-Lipschitz.

• image_inter_normalCylinder : ⇑e '' Ω ∩ TauCeti.normalCylinder h r = {x : WithLp 2 (ℝ × E) | γ x.snd < x.fst} ∩ TauCeti.normalCylinder h r

  Inside the cylinder, Ω is the region above the graph.

theorem Set.isLipschitzChart_of_forall_mem_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : Set F} {e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)} {γ : E → ℝ} {K : NNReal} {h r : ℝ} (hh : 0 < h) (hr : 0 < r) (hγ : LipschitzWith K γ) (hmem : ∀ z ∈ TauCeti.normalCylinder h r, e.symm z ∈ Ω ↔ γ z.snd < z.fst) : Ω.IsLipschitzChart e γ K h r

A chart whose cylinder meets Ω exactly above the graph of γ is a Lipschitz chart.

theorem Set.IsLipschitzChart.image_frontier_inter_normalCylinder {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : Set F} {e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)} {γ : E → ℝ} {K : NNReal} {h r : ℝ} (hc : Ω.IsLipschitzChart e γ K h r) : ⇑e '' frontier Ω ∩ TauCeti.normalCylinder h r = {x : WithLp 2 (ℝ × E) | x.fst = γ x.snd} ∩ TauCeti.normalCylinder h r

Inside the cylinder of a Lipschitz chart, the frontier of Ω is the graph.

theorem Set.IsLipschitzChart.image_closure_inter_normalCylinder {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : Set F} {e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)} {γ : E → ℝ} {K : NNReal} {h r : ℝ} (hc : Ω.IsLipschitzChart e γ K h r) : ⇑e '' closure Ω ∩ TauCeti.normalCylinder h r = {x : WithLp 2 (ℝ × E) | γ x.snd ≤ x.fst} ∩ TauCeti.normalCylinder h r

Inside the cylinder of a Lipschitz chart, the closure of Ω is the region on or above the graph.

theorem Set.IsLipschitzChart.mem_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : Set F} {e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)} {γ : E → ℝ} {K : NNReal} {h r : ℝ} (hc : Ω.IsLipschitzChart e γ K h r) {x : F} (hxC : e x ∈ TauCeti.normalCylinder h r) : x ∈ Ω ↔ γ (e x).snd < (e x).fst

A point whose image lies in the cylinder of a Lipschitz chart belongs to Ω exactly when its image lies above the graph.

theorem Set.IsLipschitzChart.fst_apply_eq_of_mem_frontier {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : Set F} {e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)} {γ : E → ℝ} {K : NNReal} {h r : ℝ} (hc : Ω.IsLipschitzChart e γ K h r) {x : F} (hx : x ∈ frontier Ω) (hxC : e x ∈ TauCeti.normalCylinder h r) : (e x).fst = γ (e x).snd

A frontier point of Ω inside the cylinder of a Lipschitz chart lies on the graph.

theorem Set.IsLipschitzChart.mono {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : Set F} {e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)} {γ : E → ℝ} {K : NNReal} {h r : ℝ} (hc : Ω.IsLipschitzChart e γ K h r) {h' r' : ℝ} (hh' : 0 < h') (hr' : 0 < r') (hh : h' ≤ h) (hr : r' ≤ r) : Ω.IsLipschitzChart e γ K h' r'

A Lipschitz chart restricts to every smaller cylinder.

theorem Set.IsLipschitzChart.weaken {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : Set F} {e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)} {γ : E → ℝ} {K : NNReal} {h r : ℝ} (hc : Ω.IsLipschitzChart e γ K h r) {K' : NNReal} (hK : K ≤ K') : Ω.IsLipschitzChart e γ K' h r

A K-Lipschitz chart is a K'-Lipschitz chart for every K' ≥ K.

theorem Set.IsLipschitzChart.trans_constVAdd {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : Set F} {e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)} {γ : E → ℝ} {K : NNReal} {h r : ℝ} (hc : Ω.IsLipschitzChart e γ K h r) (p : WithLp 2 (ℝ × E)) {h' r' : ℝ} (hh' : 0 < h') (hr' : 0 < r') (hh : |p.fst| + h' ≤ h) (hr : ‖p.snd‖ + r' ≤ r) : Ω.IsLipschitzChart (e.trans (AffineIsometryEquiv.constVAdd ℝ (WithLp 2 (ℝ × E)) (-p))) (fun (y : E) => γ (y + p.snd) - p.fst) K h' r'

Recentring a Lipschitz chart at the point p of the model: after translating by -p, the graph function becomes y ↦ γ (y + p.snd) - p.fst, and any cylinder whose translate by p lies in the original cylinder is again a chart.

theorem Set.IsLipschitzChart.exists_isLipschitzChart_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : Set F} {e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)} {γ : E → ℝ} {K : NNReal} {h r : ℝ} (hc : Ω.IsLipschitzChart e γ K h r) {x : F} (hx : e x ∈ TauCeti.normalCylinder h r) : ∃ (e' : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)) (γ' : E → ℝ) (h' : ℝ) (r' : ℝ), Ω.IsLipschitzChart e' γ' K h' r' ∧ e' x = 0

A Lipschitz chart can be recentred at any point of its cylinder, keeping its Lipschitz constant.

theorem Set.IsLipschitzChart.image {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] {Ω : Set F} {e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)} {γ : E → ℝ} {K : NNReal} {h r : ℝ} (hc : Ω.IsLipschitzChart e γ K h r) (g : F ≃ᵃⁱ[ℝ] G) : (⇑g '' Ω).IsLipschitzChart (g.symm.trans e) γ K h r

Transporting a Lipschitz chart along an affine isometry g : F ≃ᵃⁱ[ℝ] G.

theorem Set.IsLipschitzChart.smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : Set F} {e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)} {γ : E → ℝ} {K : NNReal} {h r : ℝ} (hc : Ω.IsLipschitzChart e γ K h r) {c : ℝ} (hc0 : 0 < c) : (c • Ω).IsLipschitzChart (TauCeti.dilateConj c e) (fun (y : E) => c * γ (c⁻¹ • y)) K (c * h) (c * r)

Dilating a Lipschitz chart by a factor c > 0: the dilated set c • Ω has a chart with graph function y ↦ c * γ (c⁻¹ • y), the same Lipschitz constant, and the dilated cylinder.

Lipschitz domains

def Set.IsLipschitzDomain {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (Ω : Set F) (E : Type u_4) [NormedAddCommGroup E] [NormedSpace ℝ E] : Prop

A set Ω ⊆ F is a Lipschitz domain modelled on ℝ × E if every point of its frontier is the centre of a Lipschitz boundary chart: after an affine isometry e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E) sending the point to the origin, Ω is, inside an open cylinder around the origin, the region above the graph of a Lipschitz function on E.

theorem Set.isLipschitzDomain_iff_exists_mem_normalCylinder {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : Set F} : Ω.IsLipschitzDomain E ↔ ∀ x ∈ frontier Ω, ∃ (e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)) (γ : E → ℝ) (K : NNReal) (h : ℝ) (r : ℝ), Ω.IsLipschitzChart e γ K h r ∧ e x ∈ TauCeti.normalCylinder h r

A set is a Lipschitz domain if and only if every frontier point lies in the cylinder of some Lipschitz chart, not necessarily centred at it.

theorem Set.IsLipschitzDomain.isOpen {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : Set F} (hΩ : Ω.IsLipschitzDomain E) : IsOpen Ω

A Lipschitz domain is open: none of its frontier points belong to it, since in a chart centred at such a point the origin lies on the graph rather than above it.

theorem Set.IsLipschitzDomain.image {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] {Ω : Set F} (hΩ : Ω.IsLipschitzDomain E) (g : F ≃ᵃⁱ[ℝ] G) : (⇑g '' Ω).IsLipschitzDomain E

The image of a Lipschitz domain under an affine isometry is a Lipschitz domain.

theorem Set.IsLipschitzDomain.smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : Set F} (hΩ : Ω.IsLipschitzDomain E) {c : ℝ} (hc : 0 < c) : (c • Ω).IsLipschitzDomain E

The dilation of a Lipschitz domain by a factor c > 0 is a Lipschitz domain.

theorem Set.IsLipschitzDomain.exists_finite_cover {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : Set F} (hΩ : Ω.IsLipschitzDomain E) (hcompact : IsCompact (frontier Ω)) : ∃ (K : NNReal) (m : ℕ) (e : Fin m → F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)) (γ : Fin m → E → ℝ) (h : Fin m → ℝ) (r : Fin m → ℝ), (∀ (i : Fin m), Ω.IsLipschitzChart (e i) (γ i) K (h i) (r i)) ∧ frontier Ω ⊆ ⋃ (i : Fin m), ⇑(e i) ⁻¹' TauCeti.normalCylinder (h i) (r i)

A Lipschitz domain with compact frontier has a finite cover of its frontier by the cylinders of Lipschitz charts sharing a common Lipschitz constant.

theorem Set.IsLipschitzDomain.exists_finite_cover_of_isBounded {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : Set F} [ProperSpace F] (hΩ : Ω.IsLipschitzDomain E) (hb : Bornology.IsBounded Ω) : ∃ (K : NNReal) (m : ℕ) (e : Fin m → F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)) (γ : Fin m → E → ℝ) (h : Fin m → ℝ) (r : Fin m → ℝ), (∀ (i : Fin m), Ω.IsLipschitzChart (e i) (γ i) K (h i) (r i)) ∧ frontier Ω ⊆ ⋃ (i : Fin m), ⇑(e i) ⁻¹' TauCeti.normalCylinder (h i) (r i)

A bounded Lipschitz domain in a proper space has a finite cover of its frontier by the cylinders of Lipschitz charts sharing a common Lipschitz constant.

@[simp]

theorem Set.isLipschitzDomain_image_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] {Ω : Set F} (g : F ≃ᵃⁱ[ℝ] G) : (⇑g '' Ω).IsLipschitzDomain E ↔ Ω.IsLipschitzDomain E

Being a Lipschitz domain is invariant under affine isometries.

@[simp]

theorem Set.isLipschitzDomain_smul_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : Set F} {c : ℝ} (hc : 0 < c) : (c • Ω).IsLipschitzDomain E ↔ Ω.IsLipschitzDomain E

Being a Lipschitz domain is invariant under positive dilations.

The region above a Lipschitz graph

theorem Set.isLipschitzChart_refl_setOf_lt_fst {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {γ : E → ℝ} {K : NNReal} (hγ : LipschitzWith K γ) {h r : ℝ} (hh : 0 < h) (hr : 0 < r) : {x : WithLp 2 (ℝ × E) | γ x.snd < x.fst}.IsLipschitzChart (AffineIsometryEquiv.refl ℝ (WithLp 2 (ℝ × E))) γ K h r

The identity is a Lipschitz chart, with any cylinder, of the region above the graph of a Lipschitz function.

theorem Set.isLipschitzDomain_setOf_lt_fst {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {γ : E → ℝ} {K : NNReal} (hγ : LipschitzWith K γ) : {x : WithLp 2 (ℝ × E) | γ x.snd < x.fst}.IsLipschitzDomain E

The region strictly above the graph of a Lipschitz function γ : E → ℝ is a Lipschitz domain modelled on ℝ × E.

def Set.IsLipschitzChartWith {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (Omega : Set F) (L : NNReal) (e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)) (φ : E → ℝ) (a b : ℝ) : Prop

Omega.IsLipschitzChartWith L e φ a b says that the rigid coordinates e identify Omega inside the open product cylinder normalCylinder a b with the strict epigraph of φ, where φ satisfies LipschitzWith L φ and φ 0 = 0. The centre e.symm 0 of the chart therefore lies on the graph.

The two independently positive cylinder radii retain the product geometry needed for boundary charts and permit either the normal or tangential direction to be shrunk later.

theorem Set.IsLipschitzChartWith.toIsLipschitzChart {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {Omega : Set F} {L : NNReal} {e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)} {φ : E → ℝ} {a b : ℝ} (h : Omega.IsLipschitzChartWith L e φ a b) : Omega.IsLipschitzChart e φ L a b

A centered chart is the shared geometric chart with its graph normalized at the origin.

theorem Set.IsLipschitzChart.isLipschitzChartWith {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {Omega : Set F} {L : NNReal} {e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)} {φ : E → ℝ} {a b : ℝ} (h : Omega.IsLipschitzChart e φ L a b) (hφ : φ 0 = 0) : Omega.IsLipschitzChartWith L e φ a b

A geometric chart whose graph vanishes at the origin is a centered chart.

theorem Set.isLipschitzChartWith_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (Omega : Set F) (L : NNReal) (e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)) (φ : E → ℝ) (a b : ℝ) : Omega.IsLipschitzChartWith L e φ a b ↔ 0 < a ∧ 0 < b ∧ φ 0 = 0 ∧ LipschitzWith L φ ∧ ∀ z ∈ TauCeti.normalCylinder a b, e.symm z ∈ Omega ↔ φ z.snd < z.fst

A centered Lipschitz boundary chart written out as a rigid-coordinate graph condition.

def Set.IsLipschitzDomainAtWith {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (Omega : Set F) (L : NNReal) (x : F) : Prop

A set is a Lipschitz domain at x, with graph constant at most L, if it has a Lipschitz boundary chart whose rigid coordinates take x to the origin.

theorem Set.isLipschitzDomainAtWith_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (Omega : Set F) (L : NNReal) (x : F) : Omega.IsLipschitzDomainAtWith L x ↔ ∃ (e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)) (φ : E → ℝ) (a : ℝ) (b : ℝ), e x = 0 ∧ Omega.IsLipschitzChartWith L e φ a b

The local Lipschitz-domain predicate is the existence of a chart centred at the point.

def Set.IsLipschitzDomainWith {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (Omega : Set (WithLp 2 (ℝ × E))) (L : NNReal) : Prop

An open set is a Lipschitz domain with constant L if it has a Lipschitz graph chart with that bound at every point of its frontier.

theorem Set.isLipschitzDomainWith_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (Omega : Set (WithLp 2 (ℝ × E))) (L : NNReal) : Omega.IsLipschitzDomainWith L ↔ IsOpen Omega ∧ ∀ x ∈ frontier Omega, Omega.IsLipschitzDomainAtWith L x

A set is a Lipschitz domain with constant L exactly when it is open and has a local L-Lipschitz graph chart at every frontier point.

theorem Set.IsLipschitzChartWith.lipschitzWith {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {Omega : Set F} {L : NNReal} {e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)} {φ : E → ℝ} {a b : ℝ} (h : Omega.IsLipschitzChartWith L e φ a b) : LipschitzWith L φ

The graph function of a Lipschitz boundary chart is L-Lipschitz.

theorem Set.IsLipschitzChartWith.apply_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {Omega : Set F} {L : NNReal} {e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)} {φ : E → ℝ} {a b : ℝ} (h : Omega.IsLipschitzChartWith L e φ a b) : φ 0 = 0

The graph of a Lipschitz boundary chart passes through the centre of the chart.

theorem Set.IsLipschitzChartWith.symm_mem_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {Omega : Set F} {L : NNReal} {e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)} {φ : E → ℝ} {a b : ℝ} (h : Omega.IsLipschitzChartWith L e φ a b) {z : WithLp 2 (ℝ × E)} (hz : z ∈ TauCeti.normalCylinder a b) : e.symm z ∈ Omega ↔ φ z.snd < z.fst

Membership in chart coordinates. A point z of the chart cylinder corresponds to a point of Omega exactly when it lies strictly above the graph of φ.

theorem Set.IsLipschitzChartWith.mem_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {Omega : Set F} {L : NNReal} {e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)} {φ : E → ℝ} {a b : ℝ} (h : Omega.IsLipschitzChartWith L e φ a b) {x : F} (hx : e x ∈ TauCeti.normalCylinder a b) : x ∈ Omega ↔ φ (e x).snd < (e x).fst

Membership through a chart. A point x whose coordinates e x lie in the chart cylinder belongs to Omega exactly when e x lies strictly above the graph of φ.

theorem Set.IsLipschitzChartWith.weaken {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {Omega : Set F} {L : NNReal} {e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)} {φ : E → ℝ} {a b : ℝ} (h : Omega.IsLipschitzChartWith L e φ a b) {L' : NNReal} (hLL' : L ≤ L') : Omega.IsLipschitzChartWith L' e φ a b

A Lipschitz boundary chart remains valid after increasing the allowed Lipschitz constant.

theorem Set.IsLipschitzChartWith.mono_radii {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {Omega : Set F} {L : NNReal} {e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)} {φ : E → ℝ} {a b : ℝ} (h : Omega.IsLipschitzChartWith L e φ a b) {a' b' : ℝ} (ha' : 0 < a') (hb' : 0 < b') (haa' : a' ≤ a) (hbb' : b' ≤ b) : Omega.IsLipschitzChartWith L e φ a' b'

Restriction of a chart. A Lipschitz boundary chart remains valid on every smaller cylinder with positive radii, with the same coordinates and graph.

theorem Set.IsLipschitzChartWith.exists_mono_radii_two_mul_lt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {Omega : Set F} {L : NNReal} {e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)} {φ : E → ℝ} {a b : ℝ} (h : Omega.IsLipschitzChartWith L e φ a b) : ∃ b' ≤ b, Omega.IsLipschitzChartWith L e φ a b' ∧ 2 * ↑L * b' < a

Room for reflection across the graph. Shrinking the tangential radius of a chart gives a chart with the same coordinates, graph and normal radius whose radii satisfy 2 * L * b' < a. The shortened cylinder normalCylinder (a - 2 * L * b') b' then still contains the centre, and the reflection t ↦ 2 * φ y - t across the graph keeps it inside normalCylinder a b'.

theorem Set.IsLipschitzChartWith.preimage_normalCylinder_mem_nhds {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {Omega : Set F} {L : NNReal} {e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)} {φ : E → ℝ} {a b : ℝ} (h : Omega.IsLipschitzChartWith L e φ a b) {x : F} (hx : e x = 0) : ⇑e ⁻¹' TauCeti.normalCylinder a b ∈ nhds x

The preimage of the chart cylinder is a neighbourhood of the centre of the chart.

theorem Set.IsLipschitzChartWith.image_affineIsometryEquiv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] {Omega : Set F} {L : NNReal} {e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)} {φ : E → ℝ} {a b : ℝ} (h : Omega.IsLipschitzChartWith L e φ a b) (g : F ≃ᵃⁱ[ℝ] G) : (⇑g '' Omega).IsLipschitzChartWith L (g.symm.trans e) φ a b

Rigid-coordinate transport of a chart. Composing the coordinates of a chart with the inverse of an affine isometry g gives a chart for the image of the set under g.

theorem Set.IsLipschitzDomainAtWith.mono {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {Omega : Set F} {L L' : NNReal} {x : F} (h : Omega.IsLipschitzDomainAtWith L x) (hLL' : L ≤ L') : Omega.IsLipschitzDomainAtWith L' x

A local Lipschitz-domain chart remains valid after increasing the allowed Lipschitz constant.

theorem Set.IsLipschitzDomainWith.mono {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Omega : Set (WithLp 2 (ℝ × E))} {L L' : NNReal} (h : Omega.IsLipschitzDomainWith L) (hLL' : L ≤ L') : Omega.IsLipschitzDomainWith L'

A Lipschitz domain remains one after increasing the allowed Lipschitz constant.

theorem Set.IsLipschitzDomainAtWith.image_affineIsometryEquiv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] {Omega : Set F} {L : NNReal} {x : F} (h : Omega.IsLipschitzDomainAtWith L x) (g : F ≃ᵃⁱ[ℝ] G) : (⇑g '' Omega).IsLipschitzDomainAtWith L (g x)

Transport a local Lipschitz-domain chart by an affine isometry.

theorem Set.isLipschitzDomainAtWith_image_affineIsometryEquiv_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] {Omega : Set F} {L : NNReal} {x : F} (g : F ≃ᵃⁱ[ℝ] G) : (⇑g '' Omega).IsLipschitzDomainAtWith L (g x) ↔ Omega.IsLipschitzDomainAtWith L x

The local Lipschitz-domain condition is invariant under an affine isometry.

theorem Set.IsLipschitzDomainWith.image_affineIsometryEquiv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Omega : Set (WithLp 2 (ℝ × E))} {L : NNReal} (h : Omega.IsLipschitzDomainWith L) (g : WithLp 2 (ℝ × E) ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)) : (⇑g '' Omega).IsLipschitzDomainWith L

Affine isometries preserve Lipschitz domains and their Lipschitz constant.

theorem Set.isLipschitzDomainWith_image_affineIsometryEquiv_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Omega : Set (WithLp 2 (ℝ × E))} {L : NNReal} (g : WithLp 2 (ℝ × E) ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)) : (⇑g '' Omega).IsLipschitzDomainWith L ↔ Omega.IsLipschitzDomainWith L

Being a Lipschitz domain with a fixed constant is invariant under affine isometries.

theorem Set.isLipschitzDomainWith_image_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {Omega : Set F} {L : NNReal} (g : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)) : (⇑g '' Omega).IsLipschitzDomainWith L ↔ IsOpen Omega ∧ ∀ x ∈ frontier Omega, Omega.IsLipschitzDomainAtWith L x

Lipschitz domains in another ambient space. For an affine isometry g from F onto the model space WithLp 2 (ℝ × E), the image g '' Omega is a Lipschitz domain with constant L exactly when Omega is open and has a local L-Lipschitz graph chart at each of its frontier points. This transports Lipschitz domains of the model space to sets in F, such as the complex plane, which carry no Set.IsLipschitzDomainWith predicate of their own.

theorem Set.IsLipschitzChartWith.smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {Omega : Set F} {L : NNReal} {e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)} {φ : E → ℝ} {a b : ℝ} (h : Omega.IsLipschitzChartWith L e φ a b) {c : ℝ} (hc : 0 < c) : (c • Omega).IsLipschitzChartWith L (TauCeti.dilateConj c e) (fun (y : E) => c * φ (c⁻¹ • y)) (c * a) (c * b)

Positive dilation of a chart. For c > 0, a Lipschitz boundary chart for Omega with coordinates e, graph φ and radii a, b gives a chart for c • Omega with the same Lipschitz constant, the conjugated coordinates dilateConj c e, the graph y ↦ c * φ (c⁻¹ • y) and the radii c * a, c * b.

theorem Set.IsLipschitzDomainAtWith.smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {Omega : Set F} {L : NNReal} {x : F} (h : Omega.IsLipschitzDomainAtWith L x) {c : ℝ} (hc : 0 < c) : (c • Omega).IsLipschitzDomainAtWith L (c • x)

Positive dilation of a local chart. If Omega is a Lipschitz domain at x, then c • Omega is a Lipschitz domain at c • x for every c > 0, with the same Lipschitz constant. See Set.IsLipschitzChartWith.smul for the explicit dilated chart.

theorem Set.IsLipschitzDomainWith.smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Omega : Set (WithLp 2 (ℝ × E))} {L : NNReal} (h : Omega.IsLipschitzDomainWith L) {c : ℝ} (hc : 0 < c) : (c • Omega).IsLipschitzDomainWith L

Positive dilation of a Lipschitz domain. For c > 0, the dilation c • Omega of a Lipschitz domain with constant L is a Lipschitz domain with the same constant.

theorem IsCompact.exists_finset_isLipschitzChartWith_cover {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Omega : Set (WithLp 2 (ℝ × E))} {L : NNReal} {K : Set (WithLp 2 (ℝ × E))} (hK : IsCompact K) (h : ∀ x ∈ K, Omega.IsLipschitzDomainAtWith L x) : ∃ (t : Finset (WithLp 2 (ℝ × E))) (e : WithLp 2 (ℝ × E) → WithLp 2 (ℝ × E) ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)) (φ : WithLp 2 (ℝ × E) → E → ℝ) (a : WithLp 2 (ℝ × E) → ℝ) (b : WithLp 2 (ℝ × E) → ℝ), (∀ x ∈ t, x ∈ K ∧ (e x) x = 0 ∧ Omega.IsLipschitzChartWith L (e x) (φ x) (a x) (b x)) ∧ K ⊆ ⋃ x ∈ t, ⇑(e x) ⁻¹' TauCeti.normalCylinder (a x) (b x)

Finite chart covers of compact boundary pieces. If Omega is a Lipschitz domain with constant L at every point of a compact set K, then finitely many points of K carry Lipschitz boundary charts with the common constant L whose cylinders cover K.

theorem Set.IsLipschitzDomainWith.exists_finset_isLipschitzChartWith_cover {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Omega : Set (WithLp 2 (ℝ × E))} {L : NNReal} [FiniteDimensional ℝ E] (h : Omega.IsLipschitzDomainWith L) (hb : Bornology.IsBounded Omega) : ∃ (t : Finset (WithLp 2 (ℝ × E))) (e : WithLp 2 (ℝ × E) → WithLp 2 (ℝ × E) ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)) (φ : WithLp 2 (ℝ × E) → E → ℝ) (a : WithLp 2 (ℝ × E) → ℝ) (b : WithLp 2 (ℝ × E) → ℝ), (∀ x ∈ t, x ∈ frontier Omega ∧ (e x) x = 0 ∧ Omega.IsLipschitzChartWith L (e x) (φ x) (a x) (b x)) ∧ frontier Omega ⊆ ⋃ x ∈ t, ⇑(e x) ⁻¹' TauCeti.normalCylinder (a x) (b x)

Finite chart covers of bounded Lipschitz domains. The frontier of a bounded Lipschitz domain with constant L is covered by the cylinders of finitely many Lipschitz boundary charts, centred at frontier points, all with the common Lipschitz constant L.

theorem IsCompact.exists_finset_isLipschitzChartWith_two_mul_lt_cover {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Omega : Set (WithLp 2 (ℝ × E))} {L : NNReal} {K : Set (WithLp 2 (ℝ × E))} (hK : IsCompact K) (h : ∀ x ∈ K, Omega.IsLipschitzDomainAtWith L x) : ∃ (t : Finset (WithLp 2 (ℝ × E))) (e : WithLp 2 (ℝ × E) → WithLp 2 (ℝ × E) ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)) (φ : WithLp 2 (ℝ × E) → E → ℝ) (a : WithLp 2 (ℝ × E) → ℝ) (b : WithLp 2 (ℝ × E) → ℝ), (∀ x ∈ t, x ∈ K ∧ (e x) x = 0 ∧ Omega.IsLipschitzChartWith L (e x) (φ x) (a x) (b x) ∧ 2 * ↑L * b x < a x) ∧ K ⊆ ⋃ x ∈ t, ⇑(e x) ⁻¹' TauCeti.normalCylinder (a x - 2 * ↑L * b x) (b x)

Finite covers of compact boundary pieces by shortened chart cylinders. If Omega is a Lipschitz domain with constant L at every point of a compact set K, then finitely many points of K carry Lipschitz boundary charts with the common constant L and radii satisfying 2 * L * b x < a x, whose shortened cylinders normalCylinder (a x - 2 * L * b x) (b x) cover K.

theorem Set.IsLipschitzDomainWith.exists_finset_isLipschitzChartWith_two_mul_lt_cover {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Omega : Set (WithLp 2 (ℝ × E))} {L : NNReal} [FiniteDimensional ℝ E] (h : Omega.IsLipschitzDomainWith L) (hb : Bornology.IsBounded Omega) : ∃ (t : Finset (WithLp 2 (ℝ × E))) (e : WithLp 2 (ℝ × E) → WithLp 2 (ℝ × E) ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)) (φ : WithLp 2 (ℝ × E) → E → ℝ) (a : WithLp 2 (ℝ × E) → ℝ) (b : WithLp 2 (ℝ × E) → ℝ), (∀ x ∈ t, x ∈ frontier Omega ∧ (e x) x = 0 ∧ Omega.IsLipschitzChartWith L (e x) (φ x) (a x) (b x) ∧ 2 * ↑L * b x < a x) ∧ frontier Omega ⊆ ⋃ x ∈ t, ⇑(e x) ⁻¹' TauCeti.normalCylinder (a x - 2 * ↑L * b x) (b x)

Finite covers of bounded Lipschitz domains by shortened chart cylinders. The frontier of a bounded Lipschitz domain with constant L is covered by finitely many shortened cylinders normalCylinder (a x - 2 * L * b x) (b x) of Lipschitz boundary charts, centred at frontier points, with the common constant L and radii satisfying 2 * L * b x < a x.

theorem Set.IsLipschitzDomainWith.isLipschitzDomain {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Omega : Set (WithLp 2 (ℝ × E))} {L : NNReal} (h : Omega.IsLipschitzDomainWith L) : Omega.IsLipschitzDomain E

A uniform Lipschitz bound gives the pointwise Lipschitz-domain condition.

theorem Set.isLipschitzDomain_iff_forall_exists_isLipschitzDomainAtWith {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {Omega : Set F} : Omega.IsLipschitzDomain E ↔ ∀ x ∈ frontier Omega, ∃ (L : NNReal), Omega.IsLipschitzDomainAtWith L x

Pointwise Lipschitz domains allow the graph bound to vary with the frontier point.

theorem Set.IsLipschitzDomain.exists_isLipschitzDomainWith {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {Omega : Set (WithLp 2 (ℝ × E))} (h : Omega.IsLipschitzDomain E) (hc : IsCompact (frontier Omega)) : ∃ (L : NNReal), Omega.IsLipschitzDomainWith L

A Lipschitz domain with compact frontier has a uniform Lipschitz bound: finitely many charts cover the frontier, and recentring them at each frontier point keeps their common constant.

noncomputable def TauCeti.chartEpigraph {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {φ : E → ℝ} (e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)) (hφ : Continuous φ) : TopologicalSpace.Opens F

The points whose chart coordinates lie strictly above the graph of φ.

@[simp]

theorem TauCeti.mem_chartEpigraph {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)} {φ : E → ℝ} {hφ : Continuous φ} {x : F} : x ∈ chartEpigraph e hφ ↔ φ (e x).snd < (e x).fst

Membership in the chart epigraph is the graph inequality in chart coordinates.

theorem TauCeti.coe_normalEpigraph_eq_preimage {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {φ : E → ℝ} (e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)) (hφ : Continuous φ) : ↑(normalEpigraph { toFun := φ, continuous_toFun := hφ }) = ⇑e.symm ⁻¹' ↑(chartEpigraph e hφ)

The epigraph in chart coordinates is the inverse-chart preimage of the chart epigraph.

theorem TauCeti.chartEpigraph_inter_tsupport_subset {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {Omega : Set F} {L : NNReal} {e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)} {φ : E → ℝ} {a b : ℝ} (h : Omega.IsLipschitzChartWith L e φ a b) {ψ : F → ℝ} (hs : tsupport ψ ⊆ ⇑e ⁻¹' normalCylinder a b) : ↑(chartEpigraph e ⋯) ∩ tsupport ψ ⊆ Omega

On a cutoff supported in the chart cylinder, the chart epigraph lies in the domain.

theorem TauCeti.inter_tsupport_subset_chartEpigraph {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {Omega : Set F} {L : NNReal} {e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)} {φ : E → ℝ} {a b : ℝ} (h : Omega.IsLipschitzChartWith L e φ a b) {ψ : F → ℝ} (hs : tsupport ψ ⊆ ⇑e ⁻¹' normalCylinder a b) : Omega ∩ tsupport ψ ⊆ ↑(chartEpigraph e ⋯)

On a cutoff supported in the chart cylinder, the domain lies in the chart epigraph.

theorem TauCeti.exists_isLipschitzChartWith_of_lipschitzOnWith {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {Omega : Set F} {L : NNReal} {e : F ≃ᵃⁱ[ℝ] WithLp 2 (ℝ × E)} {φ : E → ℝ} {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (hφ0 : φ 0 = 0) (hφ : LipschitzOnWith L φ (Metric.ball 0 b)) (hgraph : ∀ z ∈ normalCylinder a b, e.symm z ∈ Omega ↔ φ z.snd < z.fst) : ∃ (ψ : E → ℝ), Set.EqOn φ ψ (Metric.ball 0 b) ∧ Omega.IsLipschitzChartWith L e ψ a b

A graph that is Lipschitz only on the tangential ball of a boundary chart can be extended to a global Lipschitz graph defining the same chart, with the same constant and radii.