Finite graph-cell divisions

A division is a finite set of graph cells covering its region, with pairwise area-null intersections. No connectedness or simple-connectedness is imposed. Vertical and horizontal divisions are independent presentations. Their boundary is the integer sum of their actual four-path cell boundaries, before any cancellation or geometric comparison.

structure TauCeti.Green.Division (d : Coordinate) (D : Set ℂ) : Type

A finite type-I or type-II division, permitting disconnected regions and finite holes.

• cells : Finset GraphCell

  The finitely many graph cells presenting the region.

• covers : ⋃ K ∈ self.cells, K.region d = D
• aedisjoint : (↑self.cells).Pairwise fun (K L : GraphCell) => MeasureTheory.AEDisjoint MeasureTheory.volume (K.region d) (L.region d)

theorem TauCeti.Green.Division.ext_iff {d : Coordinate} {D : Set ℂ} {x y : Division d D} : x = y ↔ x.cells = y.cells

theorem TauCeti.Green.Division.ext {d : Coordinate} {D : Set ℂ} {x y : Division d D} (cells : x.cells = y.cells) : x = y

theorem TauCeti.Green.Division.region_subset {d : Coordinate} {D : Set ℂ} (V : Division d D) {K : GraphCell} (hK : K ∈ V.cells) : K.region d ⊆ D

Every cell of a division lies in its region.

theorem TauCeti.Green.Division.isCompact {d : Coordinate} {D : Set ℂ} (V : Division d D) : IsCompact D

A finitely divided region is compact.

theorem TauCeti.Green.Division.measurableSet {d : Coordinate} {D : Set ℂ} (V : Division d D) : MeasurableSet D

A finitely divided region is measurable.

theorem TauCeti.Green.Division.integrableOn_iff {d : Coordinate} {D : Set ℂ} (V : Division d D) {f : ℂ → ℝ} : MeasureTheory.IntegrableOn f D MeasureTheory.volume ↔ ∀ K ∈ V.cells, MeasureTheory.IntegrableOn f (K.region d) MeasureTheory.volume

Cellwise integrability is equivalent to integrability on the whole divided region.

theorem TauCeti.Green.Division.integral_eq_sum {d : Coordinate} {D : Set ℂ} (V : Division d D) {f : ℂ → ℝ} (hf : ∀ K ∈ V.cells, MeasureTheory.IntegrableOn f (K.region d) MeasureTheory.volume) : ∫ (z : ℂ) in D, f z = ∑ K ∈ V.cells, ∫ (z : ℂ) in K.region d, f z

Pairwise area-null cell overlaps make area integrals additive over the division.

noncomputable def TauCeti.Green.Division.boundary {d : Coordinate} {D : Set ℂ} (V : Division d D) : BoundaryChain

The sum of the actual signed cell-boundary chains.

Equations

• V.boundary = ∑ K ∈ V.cells, K.boundary d

theorem TauCeti.Green.Division.boundary_def {d : Coordinate} {D : Set ℂ} (V : Division d D) : V.boundary = ∑ K ∈ V.cells, K.boundary d

The division boundary is the finite sum of its oriented cell boundaries.

@[simp]

theorem TauCeti.Green.Division.boundary_boundary {d : Coordinate} {D : Set ℂ} (V : Division d D) : BoundaryChain.boundary V.boundary = 0

Every division boundary is an endpoint cycle.

def TauCeti.Green.Division.single (d : Coordinate) (K : GraphCell) : Division d (K.region d)

Every graph cell is its own one-cell division, giving nondegenerate rectangular examples.

Equations

• TauCeti.Green.Division.single d K = { cells := {K}, covers := ⋯, aedisjoint := ⋯ }

@[simp]

theorem TauCeti.Green.Division.single_cells (d : Coordinate) (K : GraphCell) : (single d K).cells = {K}

@[simp]

theorem TauCeti.Green.Division.boundary_single (d : Coordinate) (K : GraphCell) : (single d K).boundary = K.boundary d