structure EquivariantMap : Type

Equivariant maps from ℝ to itself are functions f : ℝ → ℝ with f (t + 1) = f t + 1.

• toFun : ℝ → ℝ
• eqv' (t : ℝ) : self.toFun (t + 1) = self.toFun t + 1

@[implicit_reducible]

instance EquivariantMap.instCoeFunForallReal : CoeFun EquivariantMap fun (x : EquivariantMap) => ℝ → ℝ

Equations

• EquivariantMap.instCoeFunForallReal = { coe := EquivariantMap.toFun }

theorem EquivariantMap.eqv (φ : EquivariantMap) (t : ℝ) : φ.toFun (t + 1) = φ.toFun t + 1

theorem EquivariantMap.sub_one (φ : EquivariantMap) (t : ℝ) : φ.toFun (t - 1) = φ.toFun t - 1

theorem EquivariantMap.add_coe (φ : EquivariantMap) (t : ℝ) (n : ℤ) : φ.toFun (t + ↑n) = φ.toFun t + ↑n

theorem EquivariantMap.coe_int (φ : EquivariantMap) (n : ℤ) : φ.toFun ↑n = φ.toFun 0 + ↑n

theorem EquivariantMap.one (φ : EquivariantMap) : φ.toFun 1 = φ.toFun 0 + 1

theorem EquivariantMap.not_bounded_above (φ : EquivariantMap) (y : ℝ) : ∃ (x : ℝ), y ≤ φ.toFun x

theorem EquivariantMap.not_bounded_below (φ : EquivariantMap) (y : ℝ) : ∃ (x : ℝ), φ.toFun x ≤ y

theorem EquivariantMap.coe_mk (f : ℝ → ℝ) {eqv : ∀ (t : ℝ), f (t + 1) = f t + 1} : { toFun := f, eqv' := eqv }.toFun = f

theorem EquivariantMap.surjective (φ : EquivariantMap) (h : Continuous φ.toFun) : Function.Surjective φ.toFun

theorem EquivariantMap.fract_add_floor (φ : EquivariantMap) (t : ℝ) : φ.toFun (Int.fract t) + ↑⌊t⌋ = φ.toFun t

theorem EquivariantMap.monotone (φ : EquivariantMap) (h : MonotoneOn φ.toFun unitInterval) : Monotone φ.toFun

theorem EquivariantMap.fract_fract (φ : EquivariantMap) (t : ℝ) : Int.fract (φ.toFun (Int.fract t)) = Int.fract (φ.toFun t)

noncomputable def linearReparam : EquivariantMap

continuous equivariant reparametrization that is locally constant around 0. It is piecewise linear, connecting (0, 0), (1/4, 0) and (3/4, 1) and (1, 1), and extended to an equivariant function.

Equations

• linearReparam = { toFun := fun (t : ℝ) => t + 4⁻¹ - |Int.fract (t - 4⁻¹) - 2⁻¹|, eqv' := linearReparam._proof_3 }

theorem linearReparam_eq_zero {t : ℝ} (h1 : -4⁻¹ ≤ t) (h2 : t ≤ 4⁻¹) : linearReparam.toFun t = 0

theorem linearReparam_eq_zero' {t : ℝ} (h1 : 0 ≤ t) (h2 : t ≤ 4⁻¹) : linearReparam.toFun t = 0

@[simp]

theorem linearReparam_zero : linearReparam.toFun 0 = 0

theorem linearReparam_eq_one {t : ℝ} (h1 : 3 / 4 ≤ t) (h2 : t ≤ 5 / 4) : linearReparam.toFun t = 1

theorem linearReparam_eq_one' {t : ℝ} (h1 : 3 / 4 ≤ t) (h2 : t ≤ 1) : linearReparam.toFun t = 1

@[simp]

theorem linearReparam_one : linearReparam.toFun 1 = 1

theorem linearReparam_monotone : Monotone linearReparam.toFun

theorem linearReparam_nonpos {t : ℝ} (ht : t ≤ 4⁻¹) : linearReparam.toFun t ≤ 0

theorem linearReparam_nonneg {t : ℝ} (ht : -4⁻¹ ≤ t) : 0 ≤ linearReparam.toFun t

theorem linearReparam_le_one {t : ℝ} (ht : t ≤ 5 / 4) : linearReparam.toFun t ≤ 1

theorem one_le_linearReparam {t : ℝ} (ht : 3 / 4 ≤ t) : 1 ≤ linearReparam.toFun t

@[simp]

theorem linearReparam_projI {t : ℝ} : linearReparam.toFun (projI t) = projI (linearReparam.toFun t)

@[simp]

theorem fract_linearReparam_eq_zero {t : ℝ} (h : Int.fract t ≤ 4⁻¹ ∨ 3 / 4 ≤ Int.fract t) : Int.fract (linearReparam.toFun t) = 0

theorem continuous_linearReparam : Continuous linearReparam.toFun

structure EquivariantEquivextends ℝ ≃ ℝ : Type

A bijection from ℝ to itself that fixes 0 and is equivariant with respect to the ℤ action by translations.

Morally, these are bijections of the circle ℝ / ℤ to itself.

• toFun : ℝ → ℝ
• invFun : ℝ → ℝ
• left_inv : Function.LeftInverse self.invFun self.toFun
• right_inv : Function.RightInverse self.invFun self.toFun
• map_zero' : self.toFun 0 = 0
• eqv' (t : ℝ) : self.toFun (t + 1) = self.toFun t + 1

@[implicit_reducible]

instance EquivariantEquiv.instCoeFunForallReal : CoeFun EquivariantEquiv fun (x : EquivariantEquiv) => ℝ → ℝ

Equations

• EquivariantEquiv.instCoeFunForallReal = { coe := fun (f : EquivariantEquiv) => f.toFun }

@[implicit_reducible]

instance EquivariantEquiv.hasCoeToEquiv : Coe EquivariantEquiv (ℝ ≃ ℝ)

Equations

• EquivariantEquiv.hasCoeToEquiv = { coe := EquivariantEquiv.toEquiv }

def EquivariantEquiv.equivariantMap (φ : EquivariantEquiv) : EquivariantMap

Forgetting its bijective properties, an equivariant_equiv can be regarded as an equivariant_map.

Equations

• φ.equivariantMap = { toFun := φ.toFun, eqv' := ⋯ }

@[simp]

theorem EquivariantEquiv.equivariantMap_toFun (φ : EquivariantEquiv) (a✝ : ℝ) : φ.equivariantMap.toFun a✝ = φ.toFun a✝

theorem EquivariantEquiv.eqv (φ : EquivariantEquiv) (t : ℝ) : φ.toFun (t + 1) = φ.toFun t + 1

@[simp]

theorem EquivariantEquiv.map_zero (φ : EquivariantEquiv) : φ.toFun 0 = 0

@[simp]

theorem EquivariantEquiv.map_zero'' (φ : EquivariantEquiv) : φ.toEquiv 0 = 0

@[simp]

theorem EquivariantEquiv.map_one (φ : EquivariantEquiv) : φ.toFun 1 = 1

@[implicit_reducible]

instance EquivariantEquiv.instHasUncurryForallProdReal {α : Type u_1} : Function.HasUncurry (α → EquivariantEquiv) (α × ℝ) ℝ

Equations

• EquivariantEquiv.instHasUncurryForallProdReal = { uncurry := fun (φ : α → EquivariantEquiv) (p : α × ℝ) => (φ p.1).toFun p.2 }

@[simp]

theorem EquivariantEquiv.coe_mk (f : ℝ ≃ ℝ) (h₀ : f.toFun 0 = 0) (h₁ : ∀ (t : ℝ), f.toFun (t + 1) = f.toFun t + 1) : { toEquiv := f, map_zero' := h₀, eqv' := h₁ }.toFun = ⇑f

theorem EquivariantEquiv.coe_toEquiv (e : EquivariantEquiv) : ⇑e.toEquiv = e.toFun

def EquivariantEquiv.symm (e : EquivariantEquiv) : EquivariantEquiv

The inverse of an equivariant_equiv is an equivariant_equiv.

Equations

• e.symm = { toEquiv := e.symm, map_zero' := ⋯, eqv' := ⋯ }

@[implicit_reducible]

instance EquivariantEquiv.instEquivLikeReal : EquivLike EquivariantEquiv ℝ ℝ

Equations

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

theorem EquivariantEquiv.ext {e₁ e₂ : EquivariantEquiv} (h : ∀ (x : ℝ), e₁.toFun x = e₂.toFun x) : e₁ = e₂

theorem EquivariantEquiv.ext_iff {e₁ e₂ : EquivariantEquiv} : e₁ = e₂ ↔ ∀ (x : ℝ), e₁.toFun x = e₂.toFun x

@[simp]

theorem EquivariantEquiv.symm_symm (e : EquivariantEquiv) : e.symm.symm = e

@[simp]

theorem EquivariantEquiv.apply_symm_apply (e : EquivariantEquiv) (x : ℝ) : e.toFun (e.symm.toFun x) = x

@[simp]

theorem EquivariantEquiv.symm_apply_apply (e : EquivariantEquiv) (x : ℝ) : e.symm.toFun (e.toFun x) = x