Basic definitions and properties of loops #
Definition and periodicity lemmas #
Any function φ : α → loop X
can be seen as a function α × ℝ → X
.
Equations
- Loop.Zero = { zero := Loop.const 0 }
Equations
- Loop.instInhabited = { default := Loop.const default }
@[simp]
@[simp]
Equations
- One or more equations did not get rendered due to their size.
Shifting a loop, or equivalently, adding a constant value to a loop.
@[simp]
Equations
- Loop.instModule = { toSMul := Loop.instSMul, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }
@[simp]
Support of a loop family #
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.
Instances For
From paths to loops #
Turn a path into a loop.
Instances For
@[simp]
@[simp]
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 #
The round-trip defined by γ
is γ
followed by γ⁻¹
.
Equations
- Loop.roundTrip γ = Loop.ofPath (γ.trans γ.symm)
Instances For
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)
:
noncomputable def
Loop.roundTripFamily
{X : Type u_2}
[TopologicalSpace X]
{x y : X}
(γ : Path x y)
:
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 ⋯ ⋯)
Instances For
theorem
Loop.roundTripFamily_continuous
{X : Type u_2}
[TopologicalSpace X]
{x y : X}
{γ : Path x y}
:
theorem
Loop.roundTripFamily_based_at
{X : Type u_2}
[TopologicalSpace X]
{x y : X}
{γ : Path x y}
(t : ℝ)
:
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.
Instances For
@[simp]
theorem
Loop.isConst_iff_forall_avg
{F : Type u_7}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[CompleteSpace F]
{γ : Loop F}
:
@[simp]
theorem
Loop.average_const
{F : Type u_7}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[CompleteSpace F]
{f : 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)
:
@[simp]
theorem
Loop.average_smul
{F : Type u_7}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{γ : Loop F}
{c : ℝ}
:
theorem
Loop.isConst_iff_const_avg
{F : Type u_7}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[CompleteSpace F]
{γ : Loop F}
:
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]
[FirstCountableTopology E]
[LocallyCompactSpace E]
{γ : E → Loop F}
(hγ_cont : Continuous ↿γ)
:
Continuous fun (x : E) => (γ x).average
@[simp]
theorem
Loop.normalize_apply
{F : Type u_7}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
(γ : Loop F)
(t : ℝ)
:
@[simp]
theorem
Loop.normalize_of_isConst
{F : Type u_7}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[CompleteSpace F]
{γ : Loop F}
(h : γ.IsConst)
:
Differentiation of loop families #
def
Loop.diff
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{F : Type u_7}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
(γ : E → Loop F)
(e : E)
:
Differential of a loop family with respect to the parameter.
Equations
Instances For
@[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 : ℝ)
:
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}
:
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)
:
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 ↿γ)
:
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)
:
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 ↿γ)
:
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 ↿γ)
: