def
definition
LE
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.NavierStokes.FourierExtraction on GitHub at line 61.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
58 (fun n => hf (CE f c R hf m n) (m + 1))).choose_spec.choose
59
60/-- The "local" extraction at step m+1. -/
61private noncomputable def LE (m : ℕ) : ℕ → ℕ :=
62 (bounded_subseq_tendsto (fun n => f (CE f c R hf m n) (m + 1)) c R
63 (fun n => hf (CE f c R hf m n) (m + 1))).choose
64
65private theorem CE_zero : CE f c R hf 0 =
66 (bounded_subseq_tendsto (fun n => f n 0) c R (fun n => hf n 0)).choose := rfl
67
68private theorem CE_succ (m : ℕ) : CE f c R hf (m + 1) = CE f c R hf m ∘ LE f c R hf m := rfl
69
70private theorem LE_strictMono (m : ℕ) : StrictMono (LE f c R hf m) :=
71 (bounded_subseq_tendsto (fun n => f (CE f c R hf m n) (m + 1)) c R
72 (fun n => hf (CE f c R hf m n) (m + 1))).choose_spec.choose_spec.1
73
74private theorem CE_strictMono : ∀ m, StrictMono (CE f c R hf m) := by
75 intro m; induction m with
76 | zero =>
77 exact (bounded_subseq_tendsto (fun n => f n 0) c R (fun n => hf n 0)).choose_spec.choose_spec.1
78 | succ k ih =>
79 rw [CE_succ]; exact ih.comp (LE_strictMono f c R hf k)
80
81private theorem LE_conv (m : ℕ) :
82 Tendsto (fun n => f (CE f c R hf m (LE f c R hf m n)) (m + 1)) atTop
83 (𝓝 (CL f c R hf (m + 1))) :=
84 (bounded_subseq_tendsto (fun n => f (CE f c R hf m n) (m + 1)) c R
85 (fun n => hf (CE f c R hf m n) (m + 1))).choose_spec.choose_spec.2
86
87private theorem CE_conv_at : ∀ m, Tendsto (fun n => f (CE f c R hf m n) m)
88 atTop (𝓝 (CL f c R hf m)) := by
89 intro m; cases m with
90 | zero =>
91 exact (bounded_subseq_tendsto (fun n => f n 0) c R (fun n => hf n 0)).choose_spec.choose_spec.2