Planar cells between continuous graphs

The vertical region between two graphs includes both graphs and the two endpoint fibers. The horizontal region swaps the two coordinates. Continuous graphs on the base interval suffice for compactness and a null frontier; no differentiability or absolute continuity is required.

Degenerate fibers and empty fibers are allowed by the geometric API. The coordinate API selects either cell direction and its graph parametrization.

def TauCeti.Green.verticalRegion (a b : ℝ) (lower upper : ℝ → ℝ) : Set ℂ

A closed vertical region between two real graphs over [a,b].

Equations

• TauCeti.Green.verticalRegion a b lower upper = {z : ℂ | z.re ∈ Set.Icc a b ∧ z.im ∈ Set.Icc (lower z.re) (upper z.re)}

def TauCeti.Green.horizontalRegion (a b : ℝ) (lower upper : ℝ → ℝ) : Set ℂ

A closed horizontal region between two real graphs over [a,b].

Equations

• TauCeti.Green.horizontalRegion a b lower upper = {z : ℂ | z.im ∈ Set.Icc a b ∧ z.re ∈ Set.Icc (lower z.im) (upper z.im)}

inductive TauCeti.Green.Coordinate : Type

The coordinate used by a directional Green identity.

• re : Coordinate
• im : Coordinate

def TauCeti.Green.Coordinate.orientation : Coordinate → ℤ

The sign of the ordered base and fiber coordinates relative to the positive plane.

Equations

• TauCeti.Green.Coordinate.re.orientation = 1
• TauCeti.Green.Coordinate.im.orientation = -1

@[simp]

theorem TauCeti.Green.Coordinate.orientation_re : re.orientation = 1

@[simp]

theorem TauCeti.Green.Coordinate.orientation_im : im.orientation = -1

noncomputable def TauCeti.Green.Coordinate.proj : Coordinate → ℂ →L[ℝ] ℝ

The real linear coordinate projection.

Equations

• TauCeti.Green.Coordinate.re.proj = Complex.reCLM
• TauCeti.Green.Coordinate.im.proj = Complex.imCLM

def TauCeti.Green.Coordinate.graph (d : Coordinate) (g : ℝ → ℝ) : ℝ → ℂ

A graph parametrized by the chosen coordinate.

Equations

• TauCeti.Green.Coordinate.re.graph g = fun (t : ℝ) => { re := t, im := g t }
• TauCeti.Green.Coordinate.im.graph g = fun (t : ℝ) => { re := g t, im := t }

@[simp]

theorem TauCeti.Green.Coordinate.proj_re : re.proj = Complex.reCLM

@[simp]

theorem TauCeti.Green.Coordinate.proj_im : im.proj = Complex.imCLM

@[simp]

theorem TauCeti.Green.Coordinate.graph_re_apply (g : ℝ → ℝ) (t : ℝ) : re.graph g t = { re := t, im := g t }

@[simp]

theorem TauCeti.Green.Coordinate.graph_im_apply (g : ℝ → ℝ) (t : ℝ) : im.graph g t = { re := g t, im := t }

@[simp]

theorem TauCeti.Green.Coordinate.proj_graph (d : Coordinate) (g : ℝ → ℝ) (t : ℝ) : d.proj (d.graph g t) = t

theorem TauCeti.Green.Coordinate.continuousOn_graph (d : Coordinate) {g : ℝ → ℝ} {s : Set ℝ} (hg : ContinuousOn g s) : ContinuousOn (d.graph g) s

Continuity of a graph in either coordinate.

theorem TauCeti.Green.Coordinate.differentiableAt_graph (d : Coordinate) {g : ℝ → ℝ} {t : ℝ} (hg : DifferentiableAt ℝ g t) : DifferentiableAt ℝ (d.graph g) t

A graph is differentiable at every differentiability point of its graph function.

def TauCeti.Green.Coordinate.region (d : Coordinate) (a b : ℝ) (lower upper : ℝ → ℝ) : Set ℂ

The planar region between two graphs in either base-coordinate direction.

Equations

• TauCeti.Green.Coordinate.re.region a b lower upper = TauCeti.Green.verticalRegion a b lower upper
• TauCeti.Green.Coordinate.im.region a b lower upper = TauCeti.Green.horizontalRegion a b lower upper

@[simp]

theorem TauCeti.Green.Coordinate.region_re (a b : ℝ) (lower upper : ℝ → ℝ) : re.region a b lower upper = verticalRegion a b lower upper

@[simp]

theorem TauCeti.Green.Coordinate.region_im (a b : ℝ) (lower upper : ℝ → ℝ) : im.region a b lower upper = horizontalRegion a b lower upper

theorem TauCeti.Green.Coordinate.differentiableAt_graph_comp (d : Coordinate) {g θ : ℝ → ℝ} {a b t : ℝ} {S : Set ℝ} (hg : ∀ x ∈ Set.Ioo a b \ S, DifferentiableAt ℝ g x) (hθ : DifferentiableAt ℝ θ t) (hmem : θ t ∈ Set.Icc a b) (havoid : θ t ∉ S ∪ {a, b}) : DifferentiableAt ℝ (d.graph g ∘ θ) t

A coordinate graph composed with a differentiable parameter is differentiable when its coordinate lies in the base interval and avoids the exceptional levels and endpoints.

@[simp]

theorem TauCeti.Green.mem_verticalRegion {a b : ℝ} {lower upper : ℝ → ℝ} {z : ℂ} : z ∈ verticalRegion a b lower upper ↔ z.re ∈ Set.Icc a b ∧ z.im ∈ Set.Icc (lower z.re) (upper z.re)

Membership in a vertical region in real coordinates.

@[simp]

theorem TauCeti.Green.mem_horizontalRegion {a b : ℝ} {lower upper : ℝ → ℝ} {z : ℂ} : z ∈ horizontalRegion a b lower upper ↔ z.im ∈ Set.Icc a b ∧ z.re ∈ Set.Icc (lower z.im) (upper z.im)

Membership in a horizontal region in real coordinates.

theorem TauCeti.Green.continuousOn_rectangle_of_prod {a b : ℝ × ℝ} {f : ℝ × ℝ → ℝ} (hf : ContinuousOn f (Set.Icc a b)) : ContinuousOn (fun (z : ℂ) => f (z.re, z.im)) (verticalRegion a.1 b.1 (fun (x : ℝ) => a.2) fun (x : ℝ) => b.2)

Continuous functions on a real product rectangle remain continuous in complex coordinates.

theorem TauCeti.Green.preimage_measurableEquivRealProd_symm_verticalRegion {a b : ℝ} {lower upper : ℝ → ℝ} : ⇑Complex.measurableEquivRealProd.symm ⁻¹' verticalRegion a b lower upper = {p : ℝ × ℝ | p.1 ∈ Set.Icc a b ∧ p.2 ∈ Set.Icc (lower p.1) (upper p.1)}

In real product coordinates the vertical cell has the indicated interval fibers.

theorem TauCeti.Green.verticalRegion_fiber_of_mem {a b : ℝ} {lower upper : ℝ → ℝ} {x : ℝ} (hx : x ∈ Set.Icc a b) : (fun (y : ℝ) => Complex.measurableEquivRealProd.symm (x, y)) ⁻¹' verticalRegion a b lower upper = Set.Icc (lower x) (upper x)

A fiber over a point of the base interval is exactly the closed interval between the graphs.

theorem TauCeti.Green.verticalRegion_fiber_of_notMem {a b : ℝ} {lower upper : ℝ → ℝ} {x : ℝ} (hx : x ∉ Set.Icc a b) : (fun (y : ℝ) => Complex.measurableEquivRealProd.symm (x, y)) ⁻¹' verticalRegion a b lower upper = ∅

A fiber outside the base interval is empty.

theorem TauCeti.Green.isClosed_verticalRegion {a b : ℝ} {lower upper : ℝ → ℝ} (hl : ContinuousOn lower (Set.Icc a b)) (hu : ContinuousOn upper (Set.Icc a b)) : IsClosed (verticalRegion a b lower upper)

A vertical region with continuous graphs is closed.

theorem TauCeti.Green.isCompact_verticalRegion {a b : ℝ} {lower upper : ℝ → ℝ} (hl : ContinuousOn lower (Set.Icc a b)) (hu : ContinuousOn upper (Set.Icc a b)) : IsCompact (verticalRegion a b lower upper)

A vertical region with continuous graphs is compact, even if some fibers are empty.

theorem TauCeti.Green.measurableSet_verticalRegion {a b : ℝ} {lower upper : ℝ → ℝ} (hl : ContinuousOn lower (Set.Icc a b)) (hu : ContinuousOn upper (Set.Icc a b)) : MeasurableSet (verticalRegion a b lower upper)

A vertical region with continuous graphs is measurable.

theorem TauCeti.Green.mem_interior_verticalRegion {a b : ℝ} {lower upper : ℝ → ℝ} {z : ℂ} (hl : ContinuousOn lower (Set.Icc a b)) (hu : ContinuousOn upper (Set.Icc a b)) (hx : z.re ∈ Set.Ioo a b) (hy : z.im ∈ Set.Ioo (lower z.re) (upper z.re)) : z ∈ interior (verticalRegion a b lower upper)

Points strictly between both endpoint fibers and the two graphs are interior points.

theorem TauCeti.Green.frontier_verticalRegion_subset {a b : ℝ} {lower upper : ℝ → ℝ} (hl : ContinuousOn lower (Set.Icc a b)) (hu : ContinuousOn upper (Set.Icc a b)) : frontier (verticalRegion a b lower upper) ⊆ {z : ℂ | z.re = a} ∪ {z : ℂ | z.re = b} ∪ {z : ℂ | z.re ∈ Set.Icc a b ∧ z.im = lower z.re} ∪ {z : ℂ | z.re ∈ Set.Icc a b ∧ z.im = upper z.re}

The frontier is contained in the two endpoint lines and the two graph traces.

theorem TauCeti.Green.volume_frontier_verticalRegion_eq_zero {a b : ℝ} {lower upper : ℝ → ℝ} (hl : ContinuousOn lower (Set.Icc a b)) (hu : ContinuousOn upper (Set.Icc a b)) : MeasureTheory.volume (frontier (verticalRegion a b lower upper)) = 0

The frontier of a vertical cell bounded by continuous graphs has zero planar area.

theorem TauCeti.Green.preimage_coordinateSwapCLE_verticalRegion {a b : ℝ} {lower upper : ℝ → ℝ} : ⇑Complex.coordinateSwapCLE ⁻¹' verticalRegion a b lower upper = horizontalRegion a b lower upper

The horizontal region is the coordinate swap of the vertical region.

theorem TauCeti.Green.preimage_coordinateSwapCLE_horizontalRegion {a b : ℝ} {lower upper : ℝ → ℝ} : ⇑Complex.coordinateSwapCLE ⁻¹' horizontalRegion a b lower upper = verticalRegion a b lower upper

The vertical region is the coordinate swap of the horizontal region.

theorem TauCeti.Green.isCompact_horizontalRegion {a b : ℝ} {lower upper : ℝ → ℝ} (hl : ContinuousOn lower (Set.Icc a b)) (hu : ContinuousOn upper (Set.Icc a b)) : IsCompact (horizontalRegion a b lower upper)

A horizontal region with continuous graphs is compact.

theorem TauCeti.Green.measurableSet_horizontalRegion {a b : ℝ} {lower upper : ℝ → ℝ} (hl : ContinuousOn lower (Set.Icc a b)) (hu : ContinuousOn upper (Set.Icc a b)) : MeasurableSet (horizontalRegion a b lower upper)

A horizontal region with continuous graphs is measurable.

theorem TauCeti.Green.volume_frontier_horizontalRegion_eq_zero {a b : ℝ} {lower upper : ℝ → ℝ} (hl : ContinuousOn lower (Set.Icc a b)) (hu : ContinuousOn upper (Set.Icc a b)) : MeasureTheory.volume (frontier (horizontalRegion a b lower upper)) = 0

The frontier of a horizontal cell bounded by continuous graphs has zero planar area.