Graph cells for finite directional divisions

A cell carries continuous graphs on its actual closed base interval. Their extension to the real line is the canonical constant endpoint extension. Regularity means C¹ off a finite exceptional set, with no regularity up to the exceptional points and no absolute-continuity assumption. The same cell data give either a type-I or a type-II planar cell.

structure TauCeti.Green.GraphCell : Type

A graph-cell presentation with C¹ graphs away from finitely many exceptions. Only values on the base interval are stored.

• a : ℝ

  The left endpoint of the base interval.

• b : ℝ

  The right endpoint of the base interval.

• a_lt_b : self.a < self.b
• lower : C(↑(Set.Icc self.a self.b), ℝ)

  The continuous lower graph on the base interval.

• upper : C(↑(Set.Icc self.a self.b), ℝ)

  The continuous upper graph on the base interval.

• ordered (x : ↑(Set.Icc self.a self.b)) : self.lower x ≤ self.upper x
• lower_regular : ∃ (s : Set ℝ), s.Finite ∧ ContDiffOn ℝ 1 (Set.IccExtend ⋯ ⇑self.lower) (Set.Icc self.a self.b \ s)
• upper_regular : ∃ (s : Set ℝ), s.Finite ∧ ContDiffOn ℝ 1 (Set.IccExtend ⋯ ⇑self.upper) (Set.Icc self.a self.b \ s)

theorem TauCeti.Green.GraphCell.ext {x y : GraphCell} (a : x.a = y.a) (b : x.b = y.b) (lower : x.lower ≍ y.lower) (upper : x.upper ≍ y.upper) : x = y

theorem TauCeti.Green.GraphCell.ext_iff {x y : GraphCell} : x = y ↔ x.a = y.a ∧ x.b = y.b ∧ x.lower ≍ y.lower ∧ x.upper ≍ y.upper

noncomputable def TauCeti.Green.GraphCell.lowerFun (K : GraphCell) : ℝ → ℝ

The canonical constant extension of the lower graph.

Equations

• K.lowerFun = Set.IccExtend ⋯ ⇑K.lower

noncomputable def TauCeti.Green.GraphCell.upperFun (K : GraphCell) : ℝ → ℝ

The canonical constant extension of the upper graph.

Equations

• K.upperFun = Set.IccExtend ⋯ ⇑K.upper

@[simp]

theorem TauCeti.Green.GraphCell.lowerFun_apply (K : GraphCell) {x : ℝ} (hx : x ∈ Set.Icc K.a K.b) : K.lowerFun x = K.lower ⟨x, hx⟩

@[simp]

theorem TauCeti.Green.GraphCell.upperFun_apply (K : GraphCell) {x : ℝ} (hx : x ∈ Set.Icc K.a K.b) : K.upperFun x = K.upper ⟨x, hx⟩

theorem TauCeti.Green.GraphCell.continuous_lowerFun (K : GraphCell) : Continuous K.lowerFun

The constant extension of a continuous lower graph is globally continuous.

theorem TauCeti.Green.GraphCell.continuous_upperFun (K : GraphCell) : Continuous K.upperFun

The constant extension of a continuous upper graph is globally continuous.

theorem TauCeti.Green.GraphCell.lowerFun_le_upperFun (K : GraphCell) {x : ℝ} (hx : x ∈ Set.Icc K.a K.b) : K.lowerFun x ≤ K.upperFun x

The graphs retain their pointwise order on the base interval.

theorem TauCeti.Green.GraphCell.exists_countable_differentiableAt_lowerFun (K : GraphCell) : ∃ (s : Set ℝ), s.Countable ∧ ∀ t ∈ Set.Ioo K.a K.b \ s, DifferentiableAt ℝ K.lowerFun t

Finite-exception C¹ regularity supplies the graph-arc hypothesis for the lower edge.

theorem TauCeti.Green.GraphCell.exists_countable_differentiableAt_upperFun (K : GraphCell) : ∃ (s : Set ℝ), s.Countable ∧ ∀ t ∈ Set.Ioo K.a K.b \ s, DifferentiableAt ℝ K.upperFun t

Finite-exception C¹ regularity supplies the graph-arc hypothesis for the upper edge.

noncomputable def TauCeti.Green.GraphCell.region (K : GraphCell) (d : Coordinate) : Set ℂ

The planar cell, in either base-coordinate direction.

Equations

• K.region d = d.region K.a K.b K.lowerFun K.upperFun

@[simp]

theorem TauCeti.Green.GraphCell.region_re (K : GraphCell) : K.region Coordinate.re = verticalRegion K.a K.b K.lowerFun K.upperFun

@[simp]

theorem TauCeti.Green.GraphCell.region_im (K : GraphCell) : K.region Coordinate.im = horizontalRegion K.a K.b K.lowerFun K.upperFun

theorem TauCeti.Green.GraphCell.isCompact_region (K : GraphCell) (d : Coordinate) : IsCompact (K.region d)

Every graph cell is compact.

theorem TauCeti.Green.GraphCell.measurableSet_region (K : GraphCell) (d : Coordinate) : MeasurableSet (K.region d)

Every graph cell is measurable.

noncomputable def TauCeti.Green.GraphCell.boundary (K : GraphCell) (d : Coordinate) : BoundaryChain

The actual four-path oriented boundary of a graph cell.

Equations

• K.boundary d = TauCeti.Green.BoundaryChain.cellBoundary d K.a K.b K.lowerFun K.upperFun ⋯ ⋯

theorem TauCeti.Green.GraphCell.boundary_def (K : GraphCell) (d : Coordinate) : K.boundary d = BoundaryChain.cellBoundary d K.a K.b K.lowerFun K.upperFun ⋯ ⋯

The boundary uses the canonical graph extensions and the actual four-edge cell chain.

@[simp]

theorem TauCeti.Green.GraphCell.boundary_boundary (K : GraphCell) (d : Coordinate) : BoundaryChain.boundary (K.boundary d) = 0

The graph-cell boundary is an endpoint cycle.

theorem TauCeti.Green.GraphCell.integrable_and_integral_boundary (K : GraphCell) (d : Coordinate) {P R : ℂ → ℝ} (hP : ContinuousOn P (K.region d)) (hdP : ∀ x ∈ Set.Icc K.a K.b, ∀ y ∈ Set.Ioo (K.lowerFun x) (K.upperFun x), HasDerivAt (fun (y : ℝ) => P (d.graph (fun (x : ℝ) => y) x)) (R (d.graph (fun (x : ℝ) => y) x)) y) (hR : MeasureTheory.IntegrableOn R (K.region d) MeasureTheory.volume) : BoundaryChain.Integrable d.proj P (K.boundary d) ∧ (BoundaryChain.integral d.proj P) (K.boundary d) = -↑d.orientation * ∫ (z : ℂ) in K.region d, R z

Directional Green for a finite-exception cell, including gauge boundary integrability. Only differentiation in the fiber direction is assumed of the field.

def TauCeti.Green.GraphCell.ofFunctions (a b : ℝ) (hab : a < b) (lower upper : ℝ → ℝ) (hl : ContinuousOn lower (Set.Icc a b)) (hu : ContinuousOn upper (Set.Icc a b)) (hlu : ∀ x ∈ Set.Icc a b, lower x ≤ upper x) (hdl : ∃ (s : Set ℝ), s.Finite ∧ ContDiffOn ℝ 1 lower (Set.Icc a b \ s)) (hdu : ∃ (s : Set ℝ), s.Finite ∧ ContDiffOn ℝ 1 upper (Set.Icc a b \ s)) : GraphCell

Build a cell from raw graph functions by storing only their restrictions to the base interval. Changing either function outside that interval changes no stored graph value.

Equations

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

@[simp]

theorem TauCeti.Green.GraphCell.ofFunctions_a (a b : ℝ) (hab : a < b) (lower upper : ℝ → ℝ) (hl : ContinuousOn lower (Set.Icc a b)) (hu : ContinuousOn upper (Set.Icc a b)) (hlu : ∀ x ∈ Set.Icc a b, lower x ≤ upper x) (hdl : ∃ (s : Set ℝ), s.Finite ∧ ContDiffOn ℝ 1 lower (Set.Icc a b \ s)) (hdu : ∃ (s : Set ℝ), s.Finite ∧ ContDiffOn ℝ 1 upper (Set.Icc a b \ s)) : (ofFunctions a b hab lower upper hl hu hlu hdl hdu).a = a

@[simp]

theorem TauCeti.Green.GraphCell.ofFunctions_b (a b : ℝ) (hab : a < b) (lower upper : ℝ → ℝ) (hl : ContinuousOn lower (Set.Icc a b)) (hu : ContinuousOn upper (Set.Icc a b)) (hlu : ∀ x ∈ Set.Icc a b, lower x ≤ upper x) (hdl : ∃ (s : Set ℝ), s.Finite ∧ ContDiffOn ℝ 1 lower (Set.Icc a b \ s)) (hdu : ∃ (s : Set ℝ), s.Finite ∧ ContDiffOn ℝ 1 upper (Set.Icc a b \ s)) : (ofFunctions a b hab lower upper hl hu hlu hdl hdu).b = b

@[simp]

theorem TauCeti.Green.GraphCell.ofFunctions_lower (a b : ℝ) (hab : a < b) (lower upper : ℝ → ℝ) (hl : ContinuousOn lower (Set.Icc a b)) (hu : ContinuousOn upper (Set.Icc a b)) (hlu : ∀ x ∈ Set.Icc a b, lower x ≤ upper x) (hdl : ∃ (s : Set ℝ), s.Finite ∧ ContDiffOn ℝ 1 lower (Set.Icc a b \ s)) (hdu : ∃ (s : Set ℝ), s.Finite ∧ ContDiffOn ℝ 1 upper (Set.Icc a b \ s)) (x : ↑(Set.Icc (ofFunctions a b hab lower upper hl hu hlu hdl hdu).a (ofFunctions a b hab lower upper hl hu hlu hdl hdu).b)) : (ofFunctions a b hab lower upper hl hu hlu hdl hdu).lower x = lower ↑x

@[simp]

theorem TauCeti.Green.GraphCell.ofFunctions_upper (a b : ℝ) (hab : a < b) (lower upper : ℝ → ℝ) (hl : ContinuousOn lower (Set.Icc a b)) (hu : ContinuousOn upper (Set.Icc a b)) (hlu : ∀ x ∈ Set.Icc a b, lower x ≤ upper x) (hdl : ∃ (s : Set ℝ), s.Finite ∧ ContDiffOn ℝ 1 lower (Set.Icc a b \ s)) (hdu : ∃ (s : Set ℝ), s.Finite ∧ ContDiffOn ℝ 1 upper (Set.Icc a b \ s)) (x : ↑(Set.Icc (ofFunctions a b hab lower upper hl hu hlu hdl hdu).a (ofFunctions a b hab lower upper hl hu hlu hdl hdu).b)) : (ofFunctions a b hab lower upper hl hu hlu hdl hdu).upper x = upper ↑x

def TauCeti.Green.GraphCell.rectangle (a b c e : ℝ) (hab : a < b) (hce : c ≤ e) : GraphCell

Constant graphs give all nondegenerate-base rectangles, including collapsed fibers.

Equations

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

@[simp]

theorem TauCeti.Green.GraphCell.rectangle_a (a b c e : ℝ) (hab : a < b) (hce : c ≤ e) : (rectangle a b c e hab hce).a = a

@[simp]

theorem TauCeti.Green.GraphCell.rectangle_b (a b c e : ℝ) (hab : a < b) (hce : c ≤ e) : (rectangle a b c e hab hce).b = b

@[simp]

theorem TauCeti.Green.GraphCell.rectangle_lowerFun (a b c e : ℝ) (hab : a < b) (hce : c ≤ e) : (rectangle a b c e hab hce).lowerFun = fun (x : ℝ) => c

@[simp]

theorem TauCeti.Green.GraphCell.rectangle_upperFun (a b c e : ℝ) (hab : a < b) (hce : c ≤ e) : (rectangle a b c e hab hce).upperFun = fun (x : ℝ) => e