IsFwInvariant.isInvariant
theorem IsFwInvariant.isInvariant :
∀ {τ : Type u_1} {α : Type u_2} [inst : CanonicallyOrderedAddCommMonoid τ] {ϕ : τ → α → α} {s : Set α},
IsFwInvariant ϕ s → IsInvariant ϕ s
The theorem `IsFwInvariant.isInvariant` states that for any types `τ` and `α`, given `τ` is a `CanonicallyOrderedAddCommMonoid` (which includes types like natural numbers `ℕ` or non-negative real numbers `ℝ≥0`), and for any function `ϕ` from `τ` to `α`, and any set `s` of type `α`, if the set `s` is forward-invariant under the function `ϕ` (which means the function `ϕ` maps any element of the set `s` to an element within the same set `s` for all `t` greater than or equal to 0), then it is also invariant under the function `ϕ` (which means the function `ϕ` maps any element of the set `s` to an element within the same set `s` for all `t` in `τ`).
More concisely: If `τ` is a CanonicallyOrderedAddCommMonoid and `ϕ: τ → α` maps any forward-invariant subset of `α` to itself, then `ϕ` maps any element of the subset to an element within the subset for all `t` in `τ`.
|
Flow.map_add
theorem Flow.map_add :
∀ {τ : Type u_1} [inst : AddMonoid τ] [inst_1 : TopologicalSpace τ] [inst_2 : ContinuousAdd τ] {α : Type u_2}
[inst_3 : TopologicalSpace α] (ϕ : Flow τ α) (t₁ t₂ : τ) (x : α),
ϕ.toFun (t₁ + t₂) x = ϕ.toFun t₁ (ϕ.toFun t₂ x)
This theorem, `Flow.map_add`, describes a property of a flow in topological spaces. In particular, given a type `τ` with `AddMonoid`, `TopologicalSpace`, and `ContinuousAdd` structures, and another type `α` with a `TopologicalSpace` structure, for any `Flow` `ϕ` from `τ` to `α`, and any elements `t₁`, `t₂` of `τ` and `x` of `α`, the function application of `ϕ` to the sum `t₁ + t₂` and `x` is equal to the function application of `ϕ` to `t₁` and the result of the function application of `ϕ` to `t₂` and `x`. This is essentially a statement about the continuity of the addition operation in the flow.
More concisely: For any continuous flow `ϕ` from an additive and topological space `(τ, +)` to a topological space `(α, ∅)`, the diagram commutes: `ϕ(t₁ + t₂) = ϕ(t₁) + ϕ(t₂)` for all `t₁, t₂ ∈ τ` and `ϕ(x) ∈ α`.
|
Flow.map_zero_apply
theorem Flow.map_zero_apply :
∀ {τ : Type u_1} [inst : AddMonoid τ] [inst_1 : TopologicalSpace τ] [inst_2 : ContinuousAdd τ] {α : Type u_2}
[inst_3 : TopologicalSpace α] (ϕ : Flow τ α) (x : α), ϕ.toFun 0 x = x
The theorem `Flow.map_zero_apply` states that for any type `τ` that is an add monoid as well as a topological space with continuous addition, and for any type `α` that is a topological space, if we have a flow `ϕ` from `τ` to `α` and an element `x` of type `α`, applying the flow function `ϕ.toFun` at time `0` to `x` will return `x` itself. This theorem essentially shows that the flow at time zero does not change the position of any point in the space `α`.
More concisely: For any add monoid and topological space `τ`, and any topological space `α`, if `ϕ` is a continuous flow from `τ` to `α`, then `ϕ.toFun 0 = id` on `α`, where `id` is the identity function.
|
Continuous.flow
theorem Continuous.flow :
∀ {τ : Type u_1} [inst : AddMonoid τ] [inst_1 : TopologicalSpace τ] [inst_2 : ContinuousAdd τ] {α : Type u_2}
[inst_3 : TopologicalSpace α] (ϕ : Flow τ α) {β : Type u_3} [inst_4 : TopologicalSpace β] {t : β → τ},
Continuous t → ∀ {f : β → α}, Continuous f → Continuous fun x => ϕ.toFun (t x) (f x)
This theorem, called `Continuous.flow`, is an alias of `Flow.continuous` in Lean. It states that for any type τ with an AddMonoid structure and a continuous addition, a type α, a type β, and a flow ϕ from τ to α, if function `t` from β to τ and function `f` from β to α are both continuous, then the function that takes an element x from β to the flow ϕ at point `t(x)` on `f(x)` is also continuous. This theorem asserts the continuity of the evolved function under the flow, given the continuity of initial conditions and time function.
More concisely: If `τ` is an AddMonoid with a continuous addition, `α` and `β` are types, `ϕ : τ → α` is a continuous flow, `t : β → τ`, and `f : β → α` are continuous functions, then the function that computes `ϕ (t(x))` for each `x : β` is continuous from `β` to `α`.
|
isFwInvariant_iff_isInvariant
theorem isFwInvariant_iff_isInvariant :
∀ {τ : Type u_1} {α : Type u_2} [inst : CanonicallyOrderedAddCommMonoid τ] {ϕ : τ → α → α} {s : Set α},
IsFwInvariant ϕ s ↔ IsInvariant ϕ s
This theorem states that if we have a type `τ` that is a `CanonicallyOrderedAddCommMonoid` (like the set of natural numbers `ℕ` or the set of nonnegative real numbers `ℝ≥0`), then the notions of `IsFwInvariant` and `IsInvariant` are equivalent for any function `ϕ` from `τ` to `α` to `α` and any set `s` of type `α`. In other words, a set `s` of type `α` is forward-invariant under `ϕ` (i.e., `ϕ` maps elements from `s` to `s` for all nonnegative `t` in `τ`) if and only if it is invariant under `ϕ` (i.e., `ϕ` maps elements from `s` to `s` for all `t` in `τ`).
More concisely: For any CanonicallyOrderedAddCommMonoid τ and function ϕ from τ to α to α, sets s of type α are forward-invariant and invariant under ϕ are equal.
|
Flow.continuous
theorem Flow.continuous :
∀ {τ : Type u_1} [inst : AddMonoid τ] [inst_1 : TopologicalSpace τ] [inst_2 : ContinuousAdd τ] {α : Type u_2}
[inst_3 : TopologicalSpace α] (ϕ : Flow τ α) {β : Type u_3} [inst_4 : TopologicalSpace β] {t : β → τ},
Continuous t → ∀ {f : β → α}, Continuous f → Continuous fun x => ϕ.toFun (t x) (f x)
This theorem states that for any type `τ` with an addition operation and topological structure, and a continuous addition operation, and any type `α` with a topological structure, if `ϕ` is a Flow from `τ` to `α`, then for any type `β` with a topological structure and a function `t` from `β` to `τ`, if `t` is continuous and `f` is a continuous function from `β` to `α`, then the function that maps `x` in `β` to the result of applying `ϕ.toFun` to `t(x)` and `f(x)` is also continuous. Essentially, this theorem is about preserving continuity under the operations of the Flow.
More concisely: Given types `τ` with addition, topology, and a continuous addition, `α` with topology, a continuous Flow `ϕ` from `τ` to `α`, a continuous function `t` from type `β` to `τ`, and a continuous function `f` from `β` to `α`, the function that maps `x` in `β` to `ϕ.toFun (t(x))` and `f(x)` is continuous.
|