Basic definitions and properties of loops

Definition and periodicity lemmas

structure Loop (X : Type u_2) : Type u_2

A loop is a function with domain ℝ and is periodic with period 1.

• toFun : ℝ → X
• per' (t : ℝ) : ↑self (t + 1) = ↑self t

@[implicit_reducible]

instance instCoeFunLoopForallReal (X : Type u_2) : CoeFun (Loop X) fun (x : Loop X) => ℝ → X

Equations

• instCoeFunLoopForallReal X = { coe := fun (γ : Loop X) => ↑γ }

@[implicit_reducible]

instance hasUncurryLoop (X : Type u_2) {α : Type u_9} : Function.HasUncurry (α → Loop X) (α × ℝ) X

Any function φ : α → loop X can be seen as a function α × ℝ → X.

Equations

• hasUncurryLoop X = { uncurry := fun (φ : α → Loop X) (p : α × ℝ) => ↑(φ p.1) p.2 }

theorem Loop.coe_mk {X : Type u_2} {γ : ℝ → X} (h : ∀ (t : ℝ), γ (t + 1) = γ t) : ↑{ toFun := γ, per' := h } = γ

theorem Loop.ext {X : Type u_2} {γ₁ γ₂ : Loop X} : ↑γ₁ = ↑γ₂ → γ₁ = γ₂

theorem Loop.ext_iff {X : Type u_2} {γ₁ γ₂ : Loop X} : γ₁ = γ₂ ↔ ↑γ₁ = ↑γ₂

def Loop.const {X : Type u_2} (f : X) : Loop X

The constant loop.

Equations

• Loop.const f = { toFun := fun (x : ℝ) => f, per' := ⋯ }

@[simp]

theorem Loop.const_apply {X : Type u_2} (f : X) (x✝ : ℝ) : ↑(const f) x✝ = f

@[implicit_reducible]

instance Loop.Zero {X : Type u_2} [_root_.Zero X] : _root_.Zero (Loop X)

Equations

• Loop.Zero = { zero := Loop.const 0 }

@[simp]

theorem Loop.zero_fun {X : Type u_2} [_root_.Zero X] : ↑0 = 0

@[simp]

theorem Loop.const_zero {X : Type u_2} [_root_.Zero X] : const 0 = 0

@[implicit_reducible]

instance Loop.instInhabited {X : Type u_2} [Inhabited X] : Inhabited (Loop X)

Equations

• Loop.instInhabited = { default := Loop.const default }

theorem Loop.per {X : Type u_2} (γ : Loop X) (t : ℝ) : ↑γ (t + 1) = ↑γ t

Periodicity of loops restated in terms of the function coercion.

theorem Loop.periodic {X : Type u_2} (γ : Loop X) : Function.Periodic (↑γ) 1

theorem Loop.one {X : Type u_2} (γ : Loop X) : ↑γ 1 = ↑γ 0

theorem Loop.add_nat_eq {X : Type u_2} (γ : Loop X) (t : ℝ) (n : ℕ) : ↑γ (t + ↑n) = ↑γ t

theorem Loop.add_int_eq {X : Type u_2} (γ : Loop X) (t : ℝ) (n : ℤ) : ↑γ (t + ↑n) = ↑γ t

theorem Loop.fract_eq {X : Type u_2} (γ : Loop X) (t : ℝ) : ↑γ (Int.fract t) = ↑γ t

theorem Loop.range_eq_image {X : Type u_2} (γ : Loop X) : Set.range ↑γ = ↑γ '' unitInterval

def Loop.transform {X : Type u_2} {X' : Type u_3} (γ : Loop X) (f : X → X') : Loop X'

Transforming a loop by applying function f.

Equations

• γ.transform f = { toFun := fun (t : ℝ) => f (↑γ t), per' := ⋯ }

@[simp]

theorem Loop.transform_apply {X : Type u_2} {X' : Type u_3} (γ : Loop X) (f : X → X') (t : ℝ) : ↑(γ.transform f) t = f (↑γ t)

@[implicit_reducible]

instance Loop.Add {X : Type u_2} [_root_.Add X] : _root_.Add (Loop X)

Adding two loops pointwise.

Equations

• Loop.Add = { add := fun (γ₁ γ₂ : Loop X) => { toFun := fun (t : ℝ) => ↑γ₁ t + ↑γ₂ t, per' := ⋯ } }

@[simp]

theorem Loop.Add_add_apply {X : Type u_2} [_root_.Add X] (γ₁ γ₂ : Loop X) (t : ℝ) : ↑(γ₁ + γ₂) t = ↑γ₁ t + ↑γ₂ t

@[implicit_reducible]

instance Loop.Neg {X : Type u_2} [_root_.Neg X] : _root_.Neg (Loop X)

Equations

• Loop.Neg = { neg := fun (γ : Loop X) => { toFun := fun (t : ℝ) => -↑γ t, per' := ⋯ } }

@[simp]

theorem Loop.Neg_neg_apply {X : Type u_2} [_root_.Neg X] (γ : Loop X) (t : ℝ) : ↑(-γ) t = -↑γ t

@[implicit_reducible]

instance Loop.instAddCommGroup {X : Type u_2} [AddCommGroup X] : AddCommGroup (Loop X)

Equations

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

@[implicit_reducible]

instance Loop.instVAddOfAdd {X : Type u_2} [_root_.Add X] : VAdd X (Loop X)

Shifting a loop, or equivalently, adding a constant value to a loop.

Equations

• Loop.instVAddOfAdd = { vadd := fun (x : X) (γ : Loop X) => γ.transform fun (y : X) => x + y }

@[simp]

theorem Loop.vadd_apply {X : Type u_2} [_root_.Add X] {x : X} {γ : Loop X} {t : ℝ} : ↑(x +ᵥ γ) t = x + ↑γ t

@[implicit_reducible]

instance Loop.instSMul {K : Type u_1} {X : Type u_2} [SMul K X] : SMul K (Loop X)

Multiplying a loop by a scalar value.

Equations

• Loop.instSMul = { smul := fun (k : K) (γ : Loop X) => γ.transform fun (y : X) => k • y }

@[implicit_reducible]

instance Loop.instModule {K : Type u_1} {X : Type u_2} [Semiring K] [AddCommGroup X] [Module K X] : Module K (Loop X)

Equations

• Loop.instModule = { toSMul := Loop.instSMul, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

@[simp]

theorem Loop.smul_apply {K : Type u_1} {X : Type u_2} [SMul K X] {k : K} {γ : Loop X} {t : ℝ} : ↑(k • γ) t = k • ↑γ t

def Loop.reparam {F : Type u_9} (γ : Loop F) (φ : EquivariantMap) : Loop F

Reparametrizing loop γ using an equivariant map φ.

Equations

• γ.reparam φ = { toFun := ↑γ ∘ φ.toFun, per' := ⋯ }

@[simp]

theorem Loop.reparam_apply {F : Type u_9} (γ : Loop F) (φ : EquivariantMap) (a✝ : ℝ) : ↑(γ.reparam φ) a✝ = ↑γ (φ.toFun a✝)

Support of a loop family

def Loop.IsConst {X : Type u_2} (γ : Loop X) : Prop

A loop is constant if it takes the same value at every time. See also Loop.isConst_iff_forall_avg and Loop.isConst_iff_const_avg for characterizations in terms of average values.

Equations

• γ.IsConst = ∀ (t s : ℝ), ↑γ t = ↑γ s

theorem Loop.isConst_of_eq {X : Type u_2} {γ : Loop X} {f : X} (H : ∀ (t : ℝ), ↑γ t = f) : γ.IsConst

def Loop.support {X : Type u_2} {X' : Type u_3} [TopologicalSpace X] (γ : X → Loop X') : Set X

The support of a loop family is the closure of the set of parameters where the loop is not constant.

Equations

• Loop.support γ = closure {x : X | ¬(γ x).IsConst}

theorem Loop.not_mem_support {X : Type u_2} {X' : Type u_3} [TopologicalSpace X] {γ : X → Loop X'} {x : X} (h : ∀ᶠ (y : X) in nhds x, (γ y).IsConst) : x ∉ support γ

From paths to loops

noncomputable def Loop.ofPath {X : Type u_2} [TopologicalSpace X] {x : X} (γ : Path x x) : Loop X

Turn a path into a loop.

Equations

• Loop.ofPath γ = { toFun := fun (t : ℝ) => γ.extend (Int.fract t), per' := ⋯ }

@[simp]

theorem Loop.ofPath_apply {X : Type u_2} [TopologicalSpace X] {x : X} (γ : Path x x) (t : ℝ) : ↑(ofPath γ) t = γ.extend (Int.fract t)

@[simp]

theorem Loop.range_ofPath {X : Type u_2} [TopologicalSpace X] {x : X} (γ : Path x x) : Set.range ↑(ofPath γ) = Set.range ⇑γ

theorem Continuous.ofPath {X : Type u_2} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] (x : X → Y) (t : X → ℝ) (γ : (i : X) → Path (x i) (x i)) (hγ : Continuous ↿γ) (ht : Continuous t) : Continuous fun (i : X) => ↑(Loop.ofPath (γ i)) (t i)

Loop.ofPath is continuous, general version.

theorem Loop.ofPath_continuous_family {X : Type u_2} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] {x : Y} (γ : X → Path x x) (h : Continuous ↿γ) : Continuous ↿fun (s : X) => ofPath (γ s)

Loop.ofPath is continuous, where the endpoints of γ are fixed. TODO: remove

Round trips

noncomputable def Loop.roundTrip {X : Type u_2} [TopologicalSpace X] {x y : X} (γ : Path x y) : Loop X

The round-trip defined by γ is γ followed by γ⁻¹.

Equations

• Loop.roundTrip γ = Loop.ofPath (γ.trans γ.symm)

theorem Loop.roundTrip_range {X : Type u_2} [TopologicalSpace X] {x y : X} {γ : Path x y} : Set.range ↑(roundTrip γ) = Set.range ⇑γ

theorem Loop.roundTrip_based_at {X : Type u_2} [TopologicalSpace X] {x y : X} {γ : Path x y} : ↑(roundTrip γ) 0 = x

theorem Loop.roundTrip_eq {X : Type u_2} [TopologicalSpace X] {x y x' y' : X} {γ : Path x y} {γ' : Path x' y'} (h : ∀ (s : ↑unitInterval), γ s = γ' s) : roundTrip γ = roundTrip γ'

noncomputable def Loop.roundTripFamily {X : Type u_2} [TopologicalSpace X] {x y : X} (γ : Path x y) : ℝ → Loop X

The round trip loop family associated to a path γ. For each parameter t, the loop roundTripFamily γ t backtracks at γ t.

Equations

• Loop.roundTripFamily γ = fun (t : ℝ) => Loop.roundTrip ((γ.truncate 0 t).cast ⋯ ⋯)

theorem Loop.roundTripFamily_continuous {X : Type u_2} [TopologicalSpace X] {x y : X} {γ : Path x y} : Continuous ↿(roundTripFamily γ)

theorem Loop.roundTripFamily_based_at {X : Type u_2} [TopologicalSpace X] {x y : X} {γ : Path x y} (t : ℝ) : ↑(roundTripFamily γ t) 0 = x

theorem Loop.roundTripFamily_zero {X : Type u_2} [TopologicalSpace X] {x y : X} {γ : Path x y} : roundTripFamily γ 0 = ofPath (Path.refl x)

theorem Loop.roundTripFamily_one {X : Type u_2} [TopologicalSpace X] {x y : X} {γ : Path x y} : roundTripFamily γ 1 = roundTrip γ

Average value of a loop

noncomputable def Loop.average {F : Type u_7} [NormedAddCommGroup F] [NormedSpace ℝ F] (γ : Loop F) : F

The average value of a loop.

Equations

• γ.average = ∫ (x : ℝ) in 0..1, ↑γ x

@[simp]

theorem Loop.zero_average {F : Type u_7} [NormedAddCommGroup F] [NormedSpace ℝ F] : average 0 = 0

theorem Loop.isConst_iff_forall_avg {F : Type u_7} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {γ : Loop F} : γ.IsConst ↔ ∀ (t : ℝ), ↑γ t = γ.average

@[simp]

theorem Loop.average_const {F : Type u_7} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f : F} : (const f).average = f

@[simp]

theorem Loop.average_add {F : Type u_7} [NormedAddCommGroup F] [NormedSpace ℝ F] {γ₁ γ₂ : Loop F} (hγ₁ : IntervalIntegrable (↑γ₁) MeasureTheory.volume 0 1) (hγ₂ : IntervalIntegrable (↑γ₂) MeasureTheory.volume 0 1) : (γ₁ + γ₂).average = γ₁.average + γ₂.average

@[simp]

theorem Loop.average_smul {F : Type u_7} [NormedAddCommGroup F] [NormedSpace ℝ F] {γ : Loop F} {c : ℝ} : (c • γ).average = c • γ.average

theorem Loop.isConst_iff_const_avg {F : Type u_7} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {γ : Loop F} : γ.IsConst ↔ γ = const γ.average

theorem Loop.isConst_of_not_mem_support {X : Type u_2} {F : Type u_7} [TopologicalSpace X] {γ : X → Loop F} {x : X} (hx : x ∉ support γ) : (γ x).IsConst

theorem Loop.continuous_average {F : Type u_7} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : Type u_9} [TopologicalSpace E] {γ : E → Loop F} (hγ_cont : Continuous ↿γ) : Continuous fun (x : E) => (γ x).average

noncomputable def Loop.normalize {F : Type u_7} [NormedAddCommGroup F] [NormedSpace ℝ F] (γ : Loop F) : Loop F

The normalization of a loop γ is the loop γ - γ.average.

Equations

• γ.normalize = { toFun := fun (t : ℝ) => ↑γ t - γ.average, per' := ⋯ }

@[simp]

theorem Loop.normalize_apply {F : Type u_7} [NormedAddCommGroup F] [NormedSpace ℝ F] (γ : Loop F) (t : ℝ) : ↑γ.normalize t = ↑γ t - γ.average

@[simp]

theorem Loop.normalize_of_isConst {F : Type u_7} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {γ : Loop F} (h : γ.IsConst) : γ.normalize = 0

Differentiation of loop families

noncomputable def Loop.diff {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_7} [NormedAddCommGroup F] [NormedSpace ℝ F] (γ : E → Loop F) (e : E) : Loop (E →L[ℝ] F)

Differential of a loop family with respect to the parameter.

Equations

• Loop.diff γ e = { toFun := fun (t : ℝ) => partialFDerivFst ℝ (fun (e : E) (t : ℝ) => ↑(γ e) t) e t, per' := ⋯ }

@[simp]

theorem Loop.diff_apply {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_7} [NormedAddCommGroup F] [NormedSpace ℝ F] (γ : E → Loop F) (e : E) (t : ℝ) : ↑(diff γ e) t = partialFDerivFst ℝ (fun (e : E) (t : ℝ) => ↑(γ e) t) e t

theorem Loop.continuous_diff {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_7} [NormedAddCommGroup F] [NormedSpace ℝ F] {γ : E → Loop F} (h : 𝒞 1 ↿γ) : Continuous ↿(diff γ)

theorem ContDiff.partial_loop {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_7} [NormedAddCommGroup F] [NormedSpace ℝ F] {γ : E → Loop F} {n : ℕ∞} (hγ_diff : 𝒞 ↑n ↿γ) (t : ℝ) : 𝒞 ↑n fun (e : E) => ↑(γ e) t

theorem Loop.support_diff {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_7} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {γ : E → Loop F} : support (diff γ) ⊆ support γ

theorem Loop.average_diff {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_7} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [FiniteDimensional ℝ E] {γ : E → Loop F} (hγ_diff : 𝒞 1 ↿γ) (e : E) : (diff γ e).average = D (fun (e : E) => (γ e).average) e

theorem ContDiff.loop_average {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_7} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [FiniteDimensional ℝ E] {γ : E → Loop F} {n : ℕ∞} (hγ_diff : 𝒞 ↑n ↿γ) : 𝒞 ↑n fun (e : E) => (γ e).average

theorem Loop.diff_normalize {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_7} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [FiniteDimensional ℝ E] {γ : E → Loop F} (hγ_diff : 𝒞 1 ↿γ) (e : E) : (diff γ e).normalize = diff (fun (e : E) => (γ e).normalize) e

theorem contDiff_average {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_7} [NormedAddCommGroup F] [NormedSpace ℝ F] {γ : E → Loop F} [FiniteDimensional ℝ F] [FiniteDimensional ℝ E] {n : ℕ∞} (hγ_diff : 𝒞 ↑n ↿γ) : 𝒞 ↑n fun (x : E) => (γ x).average

theorem contDiff_sub_average {E : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_7} [NormedAddCommGroup F] [NormedSpace ℝ F] {γ : E → Loop F} [FiniteDimensional ℝ F] [FiniteDimensional ℝ E] {n : ℕ∞} (hγ_diff : 𝒞 ↑n ↿γ) : 𝒞 ↑n ↿fun (x : E) (t : ℝ) => ↑(γ x) t - (γ x).average