DynamicsLimit.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

Stage topology, genuine smooth limiting dynamics, initial stage, unconditional diagonal, and limiting moments.

def OAI.ThreeTorus.StageState.coordinate line 15
instance OAI.ThreeTorus.StageState.(instance at line 17) line 17
lemma OAI.ThreeTorus.StageState.continuous_coordinate line 19
lemma OAI.ThreeTorus.StageState.continuous_vec line 20
lemma OAI.ThreeTorus.StageState.continuous_mapCont line 21
lemma OAI.ThreeTorus.StageState.continuous_orbit line 23
lemma OAI.ThreeTorus.StageState.continuous_laurent line 25
lemma OAI.ThreeTorus.StageState.finite_neighborhood_control line 31
Source documentation
Finite jets and a physical vector tolerance reach every neighborhood needed for retaining previously chosen Laurent polynomials.
```
lemma finite_neighborhood_control (s : StageState) {U : Set StageState} (hU : U ∈ 𝓝 s) :
    ∃ N : ℕ, ∃ ε > 0, ∀ t : StageState,
      dist s.vec t.vec < ε → (jetExhaustion N).Close ε s.frame s.V t.frame t.V → t ∈ U := by
…
```
Mentions: OAI.ThreeTorus.StageState, OAI.ThreeTorus.jetExhaustion
lemma OAI.ThreeTorus.smooth_diagonal_eventual_jets line 73
structure OAI.ThreeTorus.SmoothDynamics line 93
Source documentation
An actual smooth, volume preserving integer action on the physical torus. This is limit DATA constructed below, not an assumption on a stage.
```
structure SmoothDynamics where
…
```
theorem OAI.ThreeTorus.smooth_dynamics_of_jets line 104
Source documentation
Mere summable finite jet changes suffice for the genuine smooth action, including the inverse and standard volume; every fixed integer power is kept.
```
theorem smooth_dynamics_of_jets (s : ℕ → StageState) {b : ℕ → ℝ} (hb : Summable b)
    (hj : ∀ n, (jetExhaustion n).Close (b n) (s n).frame (s n).V (s (n+1)).frame (s (n+1)).V) :
    ∃ D : SmoothDynamics, ∀ k : ℤ, Tendsto (fun n => (s n).mapCont k) atTop (𝓝 (D.map k)) := by
…
```
Mentions: OAI.ThreeTorus.StageState, OAI.ThreeTorus.jetExhaustion, OAI.ThreeTorus.SmoothDynamics
theorem OAI.ThreeTorus.exists_initial_stage line 157
Source documentation
Starting the actual construction needs no dynamical oracle: two reflected angular packets on a single affine good arc have exactly Haar spectrum.
```
theorem exists_initial_stage {δ : ℝ} (hδ : 0 < δ) (hδ' : δ < 1/8) :
    ∃ s : StageState, s.δ = δ := by
…
```
Mentions: OAI.ThreeTorus.StageState
structure OAI.ThreeTorus.StageHistory line 228
Source documentation
The finite history is kept at every successor; no density or limit is part of this bookkeeping data.
```
structure StageHistory (test : ℕ → PhysicalTest) (e : ℕ → ℝ) (n : ℕ) where
…
```
Mentions: OAI.ThreeTorus.PhysicalTest
lemma OAI.ThreeTorus.StageHistory.exists_start line 238
lemma OAI.ThreeTorus.StageHistory.exists_next line 249

theorem OAI.ThreeTorus.exists_stage_diagonal line 299

Source documentation

A literal diagonal of actual stage states with simultaneously retained finite polynomials. Only the externally selected real tests occur in the input; all dynamics, packets and coefficient choices are produced by the stage.

theorem exists_stage_diagonal (test : ℕ → PhysicalTest) (e b : ℕ → ℝ)
    (he : ∀ n, 0 < e n) (hb : ∀ n, 0 < b n) :
    ∃ s : ℕ → StageState, ∃ c : ℕ → (ℤ →₀ ℂ),
      (∀ n, dist (s n).vec (s (n+1)).vec < b n) ∧
      (∀ n, (jetExhaustion n).Close (b n) (s n).frame (s n).V
        (s (n+1)).frame (s (n+1)).V) ∧
      (∀ i n, i < n → dist (test i).vec ((s n).laurent (c i)) < e i) := by
…

Mentions: OAI.ThreeTorus.PhysicalTest, OAI.ThreeTorus.StageState, OAI.ThreeTorus.jetExhaustion

lemma OAI.ThreeTorus.StageState.orbit_zero line 344
lemma OAI.ThreeTorus.StageState.orbit_comp line 349
lemma OAI.ThreeTorus.StageState.inner_vec_orbit line 356
lemma OAI.ThreeTorus.StageState.orbit_orthonormal line 370
lemma OAI.ThreeTorus.StageState.vec_norm line 380