theorem AddCircle.liftIco_coe_apply_of_periodic {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [Archimedean 𝕜] {p : 𝕜} [hp : Fact (0 < p)] (a : 𝕜) {f : 𝕜 → B} (hf : Function.Periodic f p) (x : 𝕜) : liftIco p a f ↑x = f x

theorem AddCircle.liftIoc_coe_apply_of_periodic {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [Archimedean 𝕜] {p : 𝕜} [hp : Fact (0 < p)] (a : 𝕜) {f : 𝕜 → B} (hf : Function.Periodic f p) (x : 𝕜) : liftIoc p a f ↑x = f x

theorem AddCircle.liftIco_comp_mk_eq_of_periodic {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [Archimedean 𝕜] {p : 𝕜} [hp : Fact (0 < p)] (a : 𝕜) {f : 𝕜 → B} (hf : Function.Periodic f p) : liftIco p a f ∘ QuotientAddGroup.mk = f

theorem AddCircle.liftIoc_comp_mk_eq_of_periodic {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [Archimedean 𝕜] {p : 𝕜} [hp : Fact (0 < p)] (a : 𝕜) {f : 𝕜 → B} (hf : Function.Periodic f p) : liftIoc p a f ∘ QuotientAddGroup.mk = f

theorem AddCircle.liftIco_eq_liftIco {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [Archimedean 𝕜] {p : 𝕜} [hp : Fact (0 < p)] (a a' : 𝕜) {f : 𝕜 → B} (hf : Function.Periodic f p) : liftIco p a f = liftIco p a' f

If f has period p, then every lift of f to AddCircle p is the same.

theorem AddCircle.liftIoc_eq_liftIoc {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [Archimedean 𝕜] {p : 𝕜} [hp : Fact (0 < p)] (a a' : 𝕜) {f : 𝕜 → B} (hf : Function.Periodic f p) : liftIoc p a f = liftIoc p a' f

If f has period p, then every lift of f to AddCircle p is the same.

theorem AddCircle.liftIco_eq_liftIoc {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [Archimedean 𝕜] {p : 𝕜} [hp : Fact (0 < p)] (a a' : 𝕜) {f : 𝕜 → B} (hf : Function.Periodic f p) : liftIco p a f = liftIoc p a' f

If f has period p, then every lift of f to AddCircle p is the same.

theorem AddCircle.equivAddCircle_eq {𝕜 : Type u_3} [Field 𝕜] {p q : 𝕜} [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [Archimedean 𝕜] [hp : Fact (0 < p)] [hq : Fact (0 < q)] : ⇑(equivAddCircle p q ⋯ ⋯) = fun (x : AddCircle p) => ↑(↑((equivIco p 0) x) * (p⁻¹ * q))

theorem AddCircle.continuous_equivAddCircle {𝕜 : Type u_3} [Field 𝕜] {p q : 𝕜} [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [hp : Fact (0 < p)] [hq : Fact (0 < q)] : Continuous ⇑(equivAddCircle p q ⋯ ⋯)

theorem AddCircle.measurePreserving_equivAddCircle {p q : ℝ} [hp : Fact (0 < p)] [hq : Fact (0 < q)] : MeasureTheory.MeasurePreserving (⇑(equivAddCircle p q ⋯ ⋯)) haarAddCircle haarAddCircle