Boundedness property of periodic function

The main purpose of that file it to prove

lemma Continuous.bounded_of_onePeriodic_of_isCompact {f : X → ℝ → E} (cont : Continuous ↿f)
  (hper : ∀ x, OnePeriodic (f x)) {K : Set X} (hK : IsCompact K) (hfK : ∀ x ∉ K, f x = 0) :
  ∃ C, ∀ x t, ‖f x t‖ ≤ C

This is done by introducing the quotient 𝕊₁ = ℝ/ℤ as a compact topological space. Patrick is not sure this is the optimal version.

In the first part, generalize many lemmas to any period and add to Algebra.Ring.Periodic.lean?

def ℤSubℝ : AddSubgroup ℝ

The integers as an additive subgroup of the reals.

Equations

• ℤSubℝ = (Int.castAddHom ℝ).range

def transOne : Setoid ℝ

The equivalence relation on ℝ corresponding to its partition as cosets of ℤ.

Equations

• transOne = QuotientAddGroup.leftRel ℤSubℝ

def OnePeriodic {α : Type u_1} (f : ℝ → α) : Prop

The proposition that a function on ℝ is periodic with period 1.

Equations

• OnePeriodic f = Function.Periodic f 1

theorem OnePeriodic.add_nat {α : Type u_1} {f : ℝ → α} (h : OnePeriodic f) (k : ℕ) (x : ℝ) : f (x + ↑k) = f x

theorem OnePeriodic.add_int {α : Type u_1} {f : ℝ → α} (h : OnePeriodic f) (k : ℤ) (x : ℝ) : f (x + ↑k) = f x

def 𝕊₁ : Type

The circle 𝕊₁ := ℝ/ℤ.

TODO [Yury]: use AddCircle.

Equations

• 𝕊₁ = Quotient transOne

instance inst𝕊₁TopologicalSpace : TopologicalSpace 𝕊₁

Equations

• inst𝕊₁TopologicalSpace = instTopologicalSpaceQuotient

instance inst𝕊₁Inhabited : Inhabited 𝕊₁

Equations

• inst𝕊₁Inhabited = Quotient.instInhabitedQuotient transOne

theorem transOne_rel_iff {a b : ℝ} : transOne a b ↔ ∃ (k : ℤ), b = a + ↑k

def proj𝕊₁ : ℝ → 𝕊₁

The quotient map from the reals to the circle ℝ ⧸ ℤ.

Equations

• proj𝕊₁ = Quotient.mk'

@[simp]

theorem proj𝕊₁_add_int (t : ℝ) (k : ℤ) : proj𝕊₁ (t + ↑k) = proj𝕊₁ t

def 𝕊₁.repr (x : 𝕊₁) : ℝ

The unique representative in the half-open interval [0, 1) for each coset of ℤ in ℝ, regarded as a map from the circle 𝕊₁ → ℝ.

Equations

• x.repr = Int.fract (Quotient.out x)

theorem 𝕊₁.repr_mem (x : 𝕊₁) : x.repr ∈ Set.Ico 0 1

theorem 𝕊₁.proj_repr (x : 𝕊₁) : proj𝕊₁ x.repr = x

theorem image_proj𝕊₁_Ico : proj𝕊₁ '' Set.Ico 0 1 = Set.univ

theorem image_proj𝕊₁_Icc : proj𝕊₁ '' Set.Icc 0 1 = Set.univ

theorem continuous_proj𝕊₁ : Continuous proj𝕊₁

theorem isOpenMap_proj𝕊₁ : IsOpenMap proj𝕊₁

theorem quotientMap_id_proj𝕊₁ {X : Type u_2} [TopologicalSpace X] : Topology.IsQuotientMap fun (p : X × ℝ) => (p.1, proj𝕊₁ p.2)

def OnePeriodic.lift {α : Type u_1} {f : ℝ → α} (h : OnePeriodic f) : 𝕊₁ → α

A one-periodic function on ℝ descends to a function on the circle ℝ ⧸ ℤ.

Equations

• h.lift = Quotient.lift f ⋯

instance instCompactSpace𝕊₁ : CompactSpace 𝕊₁

theorem isClosed_int : IsClosed (Set.range Int.cast)

instance instT2Space𝕊₁ : T2Space 𝕊₁

theorem Continuous.bounded_on_compact_of_onePeriodic {X : Type u_2} {E : Type u_3} [TopologicalSpace X] [NormedAddCommGroup E] {f : X → ℝ → E} (cont : Continuous ↿f) (hper : ∀ (x : X), OnePeriodic (f x)) {K : Set X} (hK : IsCompact K) : ∃ (C : ℝ), ∀ x ∈ K, ∀ (t : ℝ), ‖f x t‖ ≤ C

theorem Continuous.bounded_of_onePeriodic_of_compact {X : Type u_2} {E : Type u_3} [TopologicalSpace X] [NormedAddCommGroup E] {f : X → ℝ → E} (cont : Continuous ↿f) (hper : ∀ (x : X), OnePeriodic (f x)) {K : Set X} (hK : IsCompact K) (hfK : ∀ x ∉ K, f x = 0) : ∃ (C : ℝ), ∀ (x : X) (t : ℝ), ‖f x t‖ ≤ C