SmoothLimits.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

All-order local smooth jet limits, positive and negative iterate diagonal, cover descent, and volume preservation.

theorem OAI.ThreeTorus.smooth_of_jet_limits line 16

Source documentation

Locally uniform limits of EVERY actual spatial jet are a smooth map. The limiting derivative data are not an assumed smooth diagonal.

theorem smooth_of_jet_limits {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [NormedAddCommGroup F] [NormedSpace ℝ F]
    (f : ℕ → E → F) (hf : ∀ n, ContDiff ℝ ∞ (f n))
    (q : (d : ℕ) → E → E [×d]→L[ℝ] F)
    (hq : ∀ d, TendstoLocallyUniformly (fun n => iteratedFDeriv ℝ d (f n)) (q d) atTop) :
    ContDiff ℝ ∞ (fun x => (q 0 x).curry0) := by
…

def OAI.ThreeTorus.incrementLimit line 49
Source documentation
A canonical local limit; no pointwise convergence or smooth limit is assumed.
```
def incrementLimit {X F : Type*} [NormedAddCommGroup F] (f : ℕ → X → F) (x : X) : F :=
…
```
lemma OAI.ThreeTorus.uniform_incrementLimit line 52

theorem OAI.ThreeTorus.smooth_diagonal_of_summable_jets line 72

Source documentation

Summable changes on increasing balls and increasing derivative orders produce a genuine smooth diagonal with locally uniform convergence of ALL jets. This is the completeness step used after the finite-stage producer.

theorem smooth_diagonal_of_summable_jets {E F : Type*}
    [NormedAddCommGroup E] [NormedSpace ℝ E] [LocallyCompactSpace E]
    [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F]
    (f : ℕ → E → F) (hf : ∀ n, ContDiff ℝ ∞ (f n))
    {b : ℕ → ℝ} (hb : Summable b)
    (hstep : ∀ (n d : ℕ), d ≤ n → ∀ x : E, ‖x‖ ≤ (n:ℝ) →
      dist (iteratedFDeriv ℝ d (f (n+1)) x) (iteratedFDeriv ℝ d (f n) x) ≤ b n) :
    ∃ g : E → F, ContDiff ℝ ∞ g ∧ TendstoLocallyUniformly f g atTop ∧
      ∀ d : ℕ, TendstoLocallyUniformly (fun n => iteratedFDeriv ℝ d (f n))
        (incrementLimit (fun n => iteratedFDeriv ℝ d (f n))) atTop := by
…

Mentions: OAI.ThreeTorus.incrementLimit

lemma OAI.ThreeTorus.continuous_tripleProject line 110
lemma OAI.ThreeTorus.circle_dist_coe_le line 116
lemma OAI.ThreeTorus.tripleProject_dist_le line 120
def OAI.ThreeTorus.tripleSection line 127
lemma OAI.ThreeTorus.tripleProject_section line 129
lemma OAI.ThreeTorus.tripleSection_norm line 132
lemma OAI.ThreeTorus.descend_uniform_limit line 144
Source documentation
Local uniform cover convergence, plus the exact graph equations, descends uniformly on the compact torus. The section is only a proof device; no continuity of the measurable representatives is asserted.
```
lemma descend_uniform_limit (f : ℕ → Cover → Cover) (g : Cover → Cover)
    (F : ℕ → TripleTorus → TripleTorus)
    (hg : TendstoLocallyUniformly f g atTop)
    (hgraph : ∀ n x, tripleProject (f n x) = F n (tripleProject x)) :
    TendstoUniformly F (fun z => tripleProject (g (tripleSection z))) atTop := by
…
```
Mentions: OAI.ThreeTorus.Cover, OAI.ThreeTorus.TripleTorus, OAI.ThreeTorus.tripleProject, OAI.ThreeTorus.tripleSection
lemma OAI.ThreeTorus.descend_limit_graph line 160
def OAI.ThreeTorus.jetIndices line 184
def OAI.ThreeTorus.jetExhaustion line 187
lemma OAI.ThreeTorus.mem_jetIndices line 194
lemma OAI.ThreeTorus.jetExhaustion_close_iff line 199
lemma OAI.ThreeTorus.jetExhaustion_mono line 224
def OAI.ThreeTorus.StageState.mapCont line 235
lemma OAI.ThreeTorus.StageState.mapCont_dist_of_jets line 238
instance OAI.ThreeTorus.tripleVolume_regular line 270
lemma OAI.ThreeTorus.measurePreserving_uniform_limit line 275
Source documentation
Volume invariance is closed under uniform convergence of continuous maps on the actual compact torus. No invertibility of the limit is assumed here.
```
lemma measurePreserving_uniform_limit {F : ℕ → C(TripleTorus,TripleTorus)}
    {G : C(TripleTorus,TripleTorus)} (hG : Tendsto F atTop (𝓝 G))
    (hF : ∀ n, MeasurePreserving (F n) tripleVolume tripleVolume) :
    MeasurePreserving G tripleVolume tripleVolume := by
…
```
Mentions: OAI.ThreeTorus.TripleTorus, OAI.ThreeTorus.tripleVolume