Integer chains of planar paths

An arc is an existing Path with its endpoints retained. Chains are finitely supported integer coefficients on these arcs. The endpoint boundary is terminal minus initial endpoint. The coordinate integral is the integer-linear extension of the actual Henstock integral. Integrable records genuine gauge integrability on every arc with nonzero coefficient.

@[reducible, inline]

abbrev TauCeti.Green.Arc : Type

Existing planar paths, with their endpoints.

Equations

• TauCeti.Green.Arc = ((p : ℂ) × (q : ℂ) × Path p q)

@[reducible, inline]

abbrev TauCeti.Green.BoundaryChain : Type

Finite integer-weighted sums of parameterized planar arcs.

Equations

• TauCeti.Green.BoundaryChain = (TauCeti.Green.Arc →₀ ℤ)

noncomputable def TauCeti.Green.BoundaryChain.ofPath {p q : ℂ} (γ : Path p q) : BoundaryChain

A path with coefficient one.

Equations

• TauCeti.Green.BoundaryChain.ofPath γ = Finsupp.single ⟨p, ⟨q, γ⟩⟩ 1

theorem TauCeti.Green.BoundaryChain.ofPath_def {p q : ℂ} (γ : Path p q) : ofPath γ = Finsupp.single ⟨p, ⟨q, γ⟩⟩ 1

A path generator is the singleton coefficient function on its endpoint-indexed path.

theorem TauCeti.Green.BoundaryChain.ofPath_congr {p q p' q' : ℂ} (γ : Path p q) (δ : Path p' q') (h : ∀ (t : ↑unitInterval), γ t = δ t) : ofPath γ = ofPath δ

Pointwise equal paths give the same generator, even when their endpoint indices differ.

@[simp]

theorem TauCeti.Green.BoundaryChain.support_ofPath {p q : ℂ} (γ : Path p q) : (ofPath γ).support = {⟨p, ⟨q, γ⟩⟩}

noncomputable def TauCeti.Green.BoundaryChain.boundary : BoundaryChain →ₗ[ℤ] ℂ →₀ ℤ

The endpoint boundary of a chain: terminal endpoint minus initial endpoint.

Equations

• TauCeti.Green.BoundaryChain.boundary = Finsupp.linearCombination ℤ fun (γ : TauCeti.Green.Arc) => Finsupp.single γ.snd.fst 1 - Finsupp.single γ.fst 1

theorem TauCeti.Green.BoundaryChain.boundary_apply (c : BoundaryChain) : boundary c = Finsupp.sum c fun (γ : Arc) (n : ℤ) => n • (Finsupp.single γ.snd.fst 1 - Finsupp.single γ.fst 1)

The endpoint boundary is the finite weighted sum of the endpoint differences.

@[simp]

theorem TauCeti.Green.BoundaryChain.boundary_ofPath {p q : ℂ} (γ : Path p q) : boundary (ofPath γ) = Finsupp.single q 1 - Finsupp.single p 1

noncomputable def TauCeti.Green.BoundaryChain.quadrilateral {p₀ p₁ p₂ p₃ : ℂ} (bottom : Path p₀ p₁) (right : Path p₁ p₂) (top : Path p₃ p₂) (left : Path p₀ p₃) : BoundaryChain

Four edges with the lower and right edges positive and the upper and left edges negative.

Equations

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

theorem TauCeti.Green.BoundaryChain.quadrilateral_def {p₀ p₁ p₂ p₃ : ℂ} (bottom : Path p₀ p₁) (right : Path p₁ p₂) (top : Path p₃ p₂) (left : Path p₀ p₃) : quadrilateral bottom right top left = ofPath bottom + ofPath right - ofPath top - ofPath left

The four signed edges of a quadrilateral.

@[simp]

theorem TauCeti.Green.BoundaryChain.boundary_quadrilateral {p₀ p₁ p₂ p₃ : ℂ} (bottom : Path p₀ p₁) (right : Path p₁ p₂) (top : Path p₃ p₂) (left : Path p₀ p₃) : boundary (quadrilateral bottom right top left) = 0

Every such four-edge boundary is an endpoint cycle, including degenerate edges.

noncomputable def TauCeti.Green.BoundaryChain.arcIntegral (L : ℂ →L[ℝ] ℝ) (P : ℂ → ℝ) (γ : Arc) : ℝ

Gauge integral of a coordinate one-form along one arc.

Equations

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

theorem TauCeti.Green.BoundaryChain.arcIntegral_def (L : ℂ →L[ℝ] ℝ) (P : ℂ → ℝ) (γ : Arc) : arcIntegral L P γ = BoxIntegral.integral (BoxIntegral.intervalBox 0 1 ⋯) BoxIntegral.IntegrationParams.Henstock (fun (t : Fin 1 → ℝ) => P (γ.snd.snd.extend (t 0)) * L (deriv (⇑γ.snd.snd.extend) (t 0))) BoxIntegral.BoxAdditiveMap.volume

The arc integral uses the canonical constant extension of the existing path.

noncomputable def TauCeti.Green.BoundaryChain.integral (L : ℂ →L[ℝ] ℝ) (P : ℂ → ℝ) : BoundaryChain →ₗ[ℤ] ℝ

Integer-linear extension of the gauge coordinate integral to finite chains.

Equations

• TauCeti.Green.BoundaryChain.integral L P = Finsupp.linearCombination ℤ (TauCeti.Green.BoundaryChain.arcIntegral L P)

theorem TauCeti.Green.BoundaryChain.integral_apply (L : ℂ →L[ℝ] ℝ) (P : ℂ → ℝ) (c : BoundaryChain) : (integral L P) c = Finsupp.sum c fun (γ : Arc) (n : ℤ) => n • arcIntegral L P γ

Evaluation of the chain integral as a finite integer-weighted sum.

@[simp]

theorem TauCeti.Green.BoundaryChain.integral_ofPath (L : ℂ →L[ℝ] ℝ) (P : ℂ → ℝ) {p q : ℂ} (γ : Path p q) : (integral L P) (ofPath γ) = arcIntegral L P ⟨p, ⟨q, γ⟩⟩

def TauCeti.Green.BoundaryChain.Integrable (L : ℂ →L[ℝ] ℝ) (P : ℂ → ℝ) (c : BoundaryChain) : Prop

Every nonzero arc coefficient has an actual Henstock-integrable coordinate integrand.

Equations

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

theorem TauCeti.Green.BoundaryChain.integrable_iff (L : ℂ →L[ℝ] ℝ) (P : ℂ → ℝ) (c : BoundaryChain) : Integrable L P c ↔ ∀ γ ∈ c.support, BoxIntegral.Integrable (BoxIntegral.intervalBox 0 1 ⋯) BoxIntegral.IntegrationParams.Henstock (fun (t : Fin 1 → ℝ) => P (γ.snd.snd.extend (t 0)) * L (deriv (⇑γ.snd.snd.extend) (t 0))) BoxIntegral.BoxAdditiveMap.volume

Integrability is checked exactly on the finite support of a chain.

@[simp]

theorem TauCeti.Green.BoundaryChain.integrable_zero (L : ℂ →L[ℝ] ℝ) (P : ℂ → ℝ) : Integrable L P 0

@[simp]

theorem TauCeti.Green.BoundaryChain.integrable_ofPath_iff (L : ℂ →L[ℝ] ℝ) (P : ℂ → ℝ) {p q : ℂ} (γ : Path p q) : Integrable L P (ofPath γ) ↔ BoxIntegral.Integrable (BoxIntegral.intervalBox 0 1 ⋯) BoxIntegral.IntegrationParams.Henstock (fun (t : Fin 1 → ℝ) => P (γ.extend (t 0)) * L (deriv (⇑γ.extend) (t 0))) BoxIntegral.BoxAdditiveMap.volume

theorem TauCeti.Green.BoundaryChain.Integrable.add {L : ℂ →L[ℝ] ℝ} {P : ℂ → ℝ} {c d : BoundaryChain} (hc : Integrable L P c) (hd : Integrable L P d) : Integrable L P (c + d)

Finite chain addition preserves gauge integrability, including cancellation.

@[simp]

theorem TauCeti.Green.BoundaryChain.integrable_neg_iff {L : ℂ →L[ℝ] ℝ} {P : ℂ → ℝ} {c : BoundaryChain} : Integrable L P (-c) ↔ Integrable L P c

theorem TauCeti.Green.BoundaryChain.Integrable.sub {L : ℂ →L[ℝ] ℝ} {P : ℂ → ℝ} {c d : BoundaryChain} (hc : Integrable L P c) (hd : Integrable L P d) : Integrable L P (c - d)

Chain subtraction preserves gauge integrability.

theorem TauCeti.Green.BoundaryChain.Integrable.sum {L : ℂ →L[ℝ] ℝ} {P : ℂ → ℝ} {ι : Type u_1} (s : Finset ι) (c : ι → BoundaryChain) (h : ∀ i ∈ s, Integrable L P (c i)) : Integrable L P (∑ i ∈ s, c i)

Integrability of a finite family of chains gives integrability of their sum.

theorem TauCeti.Green.BoundaryChain.Integrable.zsmul {L : ℂ →L[ℝ] ℝ} {P : ℂ → ℝ} {c : BoundaryChain} (hc : Integrable L P c) (n : ℤ) : Integrable L P (n • c)

Gauge integrability is stable under integer coefficients.

theorem TauCeti.Green.BoundaryChain.Integrable.hasIntegral {L : ℂ →L[ℝ] ℝ} {P : ℂ → ℝ} {c : BoundaryChain} (hc : Integrable L P c) {γ : Arc} (hγ : γ ∈ c.support) : BoxIntegral.HasIntegral (BoxIntegral.intervalBox 0 1 ⋯) BoxIntegral.IntegrationParams.Henstock (fun (t : Fin 1 → ℝ) => P (γ.snd.snd.extend (t 0)) * L (deriv (⇑γ.snd.snd.extend) (t 0))) BoxIntegral.BoxAdditiveMap.volume (arcIntegral L P γ)

Every supported arc has the gauge integral used by the chain integral.