Existence, pathIntegral, path algebra and linearity (CC6)

Unit: paths-and-integrals (docs/design/paths-and-integrals.md §3). Chain-continuation existence of a primitive along a path (via ChartChain), the definition of pathIntegral, and its basic algebra: trans/symm/reparam/cast invariance and ℂ-linearity in the form.

Main declarations:

• RS.IsPrimitiveAlong γ η F, RS.exists_isPrimitiveAlong, RS.pathIntegral, RS.IsPrimitiveAlong.pathIntegral_eq.
• RS.pathIntegral_refl/symm/trans/reparam/cast.
• RS.pathIntegral_add/smul/zero_form, RS.pathIntegralₗ.

The real-line clamp to [0,1]

def RS.clampI (u : ℝ) : ℝ

Clamp a real number into [0,1].

Equations

• RS.clampI u = max 0 (min u 1)

theorem RS.clampI_mem (u : ℝ) : clampI u ∈ Set.Icc 0 1

theorem RS.continuous_clampI : Continuous clampI

theorem RS.clampI_zero : clampI 0 = 0

theorem RS.clampI_one : clampI 1 = 1

theorem RS.extend_clampI {X : Type u_1} [TopologicalSpace X] {x y : X} (γ : Path x y) (u : ℝ) : γ.extend (clampI u) = γ.extend u

γ.extend is invariant under clamping its argument into [0,1].

IsPrimitiveAlong, existence, pathIntegral

def RS.IsPrimitiveAlong {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {x y : X} (γ : Path x y) (η : Form1 X) (F : ℝ → ℂ) : Prop

F is a primitive of η along the path γ.

Equations

• RS.IsPrimitiveAlong γ η F = RS.IsPrimitiveAlongMap (⇑γ.extend) η F Set.univ

theorem RS.exists_isPrimitiveAlong {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {x y : X} (γ : Path x y) (η : Form1 X) : ∃ (F : ℝ → ℂ), IsPrimitiveAlong γ η F ∧ F 0 = 0

noncomputable def RS.pathIntegral {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {x y : X} (γ : Path x y) (η : Form1 X) : ℂ

The integral of η along γ, defined via the (well-defined, see pathIntegral_eq) chosen primitive: pathIntegral γ η = F 1 - F 0.

Equations

• RS.pathIntegral γ η = ⋯.choose 1

theorem RS.IsPrimitiveAlong.pathIntegral_eq {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {x y : X} {γ : Path x y} {η : Form1 X} {F : ℝ → ℂ} (hF : IsPrimitiveAlong γ η F) : pathIntegral γ η = F 1 - F 0

Path algebra

@[simp]

theorem RS.pathIntegral_refl {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (x : X) (η : Form1 X) : pathIntegral (Path.refl x) η = 0

@[simp]

theorem RS.pathIntegral_symm {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {x y : X} (γ : Path x y) (η : Form1 X) : pathIntegral γ.symm η = -pathIntegral γ η

theorem RS.pathIntegral_trans {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {x y z : X} (γ : Path x y) (γ' : Path y z) (η : Form1 X) : pathIntegral (γ.trans γ') η = pathIntegral γ η + pathIntegral γ' η

theorem RS.pathIntegral_reparam {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {x y : X} (γ : Path x y) {f : ↑unitInterval → ↑unitInterval} (hf : Continuous f) (h₀ : f 0 = 0) (h₁ : f 1 = 1) (η : Form1 X) : pathIntegral (γ.reparam f hf h₀ h₁) η = pathIntegral γ η

@[simp]

theorem RS.pathIntegral_cast {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {x y x' y' : X} (γ : Path x y) (hx : x' = x) (hy : y' = y) (η : Form1 X) : pathIntegral (γ.cast hx hy) η = pathIntegral γ η

ℂ-linearity in the form

theorem RS.pathIntegral_add {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {x y : X} (γ : Path x y) (η θ : Form1 X) : pathIntegral γ (η + θ) = pathIntegral γ η + pathIntegral γ θ

theorem RS.pathIntegral_smul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {x y : X} (γ : Path x y) (c : ℂ) (η : Form1 X) : pathIntegral γ (c • η) = c * pathIntegral γ η

@[simp]

theorem RS.pathIntegral_zero_form {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {x y : X} (γ : Path x y) : pathIntegral γ 0 = 0

noncomputable def RS.pathIntegralₗ {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {x y : X} (γ : Path x y) : Form1 X →ₗ[ℂ] ℂ

The integral of a fixed path, as a ℂ-linear map on 1-forms.

Equations

• RS.pathIntegralₗ γ = { toFun := fun (η : RS.Form1 X) => RS.pathIntegral γ η, map_add' := ⋯, map_smul' := ⋯ }