IndisputableMonolith.ClassicalBridge.Fluids.Regularity2D
IndisputableMonolith/ClassicalBridge/Fluids/Regularity2D.lean · 320 lines · 10 declarations
show as:
view math explainer →
1import IndisputableMonolith.ClassicalBridge.Fluids.Galerkin2D
2import IndisputableMonolith.ClassicalBridge.Fluids.LNALSemantics
3import IndisputableMonolith.ClassicalBridge.Fluids.Simulation2D
4import IndisputableMonolith.ClassicalBridge.Fluids.CPM2D
5import IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D
6
7namespace IndisputableMonolith.ClassicalBridge.Fluids
8
9/-!
10# Regularity2D (Milestone M6)
11
12This file provides the **top-level composition theorem** for the 2D pipeline:
13
14Galerkin2D (M1) + LNAL encoding/semantics (M2) + one-step simulation (M3) +
15CPM instantiation (M4) + continuum limit packaging (M5)
16⇒ an abstract “continuum solution exists” conclusion.
17
18At this milestone the goal is architectural: we make the dependency graph explicit and
19compose the previously packaged hypotheses **without** using `sorry` or `axiom`.
20-/
21
22namespace Regularity2D
23
24open ContinuumLimit2D
25
26/-!
27## Master hypothesis: all ingredients of the 2D pipeline
28-/
29
30structure RSNS2DPipelineHypothesis where
31 /-- Uniform-in-`N` bounds for the Galerkin family. -/
32 Hbounds : UniformBoundsHypothesis
33 /-- Convergence to a limit Fourier trajectory. -/
34 Hconv : ConvergenceHypothesis Hbounds
35 /-- Identification: the limit satisfies a chosen solution concept. -/
36 Hid : IdentificationHypothesis Hconv
37
38/-!
39## Top-level theorem (2D)
40-/
41
42/-- RS → (abstract) global regularity in 2D, via the composed bridge pipeline.
43
44At this stage, “regularity” is represented by the existence of a limit Fourier trajectory
45`u : ℝ → FourierState2D` together with the packaged identification property.
46-/
47theorem rs_implies_global_regularity_2d
48 (H : RSNS2DPipelineHypothesis) :
49 ∃ u : ℝ → FourierState2D,
50 (∀ t : ℝ, ∀ k : Mode2,
51 Filter.Tendsto (fun N : ℕ => (extendByZero (H.Hbounds.uN N t)) k) Filter.atTop
52 (nhds ((u t) k)))
53 ∧ H.Hid.IsSolution u
54 ∧ (∀ t ≥ 0, ∀ k : Mode2, ‖(u t) k‖ ≤ H.Hbounds.B) := by
55 -- The result is exactly the continuum limit theorem from M5.
56 simpa using (continuum_limit_exists H.Hbounds H.Hconv H.Hid)
57
58/-- Variant of the top-level theorem where the “identification” is the **proved** coefficient bound:
59we do not need a separate `IdentificationHypothesis` argument for this minimal `IsSolution` notion. -/
60theorem rs_implies_global_regularity_2d_coeffBound
61 (Hbounds : UniformBoundsHypothesis)
62 (Hconv : ConvergenceHypothesis Hbounds) :
63 ∃ u : ℝ → FourierState2D,
64 (∀ t : ℝ, ∀ k : Mode2,
65 Filter.Tendsto (fun N : ℕ => (extendByZero (Hbounds.uN N t)) k) Filter.atTop
66 (nhds ((u t) k)))
67 ∧ (∀ t ≥ 0, ∀ k : Mode2, ‖(u t) k‖ ≤ Hbounds.B) := by
68 -- Take the limit object from convergence, and use the derived bound lemma.
69 refine ⟨Hconv.u, ?_, ?_⟩
70 · simpa using Hconv.converges
71 · intro t ht k
72 simpa using (ConvergenceHypothesis.coeff_bound_of_uniformBounds (HC := Hconv) t ht k)
73
74/-- Variant of the top-level theorem where the derived “identification” is:
75
76- the **proved** coefficient bound (from uniform bounds + convergence), and
77- the **proved** divergence-free constraint (passed to the limit under modewise convergence),
78 assuming each approximant is divergence-free in Fourier variables.
79
80This avoids providing a separate `IdentificationHypothesis`. -/
81theorem rs_implies_global_regularity_2d_divFreeCoeffBound
82 (Hbounds : UniformBoundsHypothesis)
83 (Hconv : ConvergenceHypothesis Hbounds)
84 (hDF : ∀ N : ℕ, ∀ t : ℝ, ∀ k : Mode2,
85 divConstraint k ((extendByZero (Hbounds.uN N t)) k) = 0) :
86 ∃ u : ℝ → FourierState2D,
87 (∀ t : ℝ, ∀ k : Mode2,
88 Filter.Tendsto (fun N : ℕ => (extendByZero (Hbounds.uN N t)) k) Filter.atTop
89 (nhds ((u t) k)))
90 ∧ (∀ t ≥ 0, ∀ k : Mode2, ‖(u t) k‖ ≤ Hbounds.B)
91 ∧ IsDivergenceFreeTraj u := by
92 refine ⟨Hconv.u, ?_, ?_, ?_⟩
93 · simpa using Hconv.converges
94 · intro t ht k
95 simpa using (ConvergenceHypothesis.coeff_bound_of_uniformBounds (HC := Hconv) t ht k)
96 · exact ConvergenceHypothesis.divFree_of_forall (HC := Hconv) hDF
97
98/-- Variant of the top-level theorem where the derived “identification” is:
99
100- the **proved** coefficient bound (from uniform bounds + convergence), and
101- the **proved** linear Stokes/heat mild identity (passed to the limit under modewise convergence),
102 assuming each approximant satisfies the same identity modewise for `t ≥ 0`.
103
104This avoids providing a separate `IdentificationHypothesis`. -/
105theorem rs_implies_global_regularity_2d_stokesMildCoeffBound
106 (Hbounds : UniformBoundsHypothesis)
107 (Hconv : ConvergenceHypothesis Hbounds)
108 (ν : ℝ)
109 (hMild :
110 ∀ N : ℕ, ∀ t ≥ 0, ∀ k : Mode2,
111 (extendByZero (Hbounds.uN N t) k) =
112 (heatFactor ν t k) • (extendByZero (Hbounds.uN N 0) k)) :
113 ∃ u : ℝ → FourierState2D,
114 (∀ t : ℝ, ∀ k : Mode2,
115 Filter.Tendsto (fun N : ℕ => (extendByZero (Hbounds.uN N t)) k) Filter.atTop
116 (nhds ((u t) k)))
117 ∧ (∀ t ≥ 0, ∀ k : Mode2, ‖(u t) k‖ ≤ Hbounds.B)
118 ∧ IsStokesMildTraj ν u := by
119 refine ⟨Hconv.u, ?_, ?_, ?_⟩
120 · simpa using Hconv.converges
121 · intro t ht k
122 simpa using (ConvergenceHypothesis.coeff_bound_of_uniformBounds (HC := Hconv) t ht k)
123 · exact ConvergenceHypothesis.stokesMild_of_forall (HC := Hconv) (ν := ν) hMild
124
125/-- Same as `rs_implies_global_regularity_2d_stokesMildCoeffBound`, but returns the **differential**
126(within `t ≥ 0`) Stokes/heat equation per mode.
127
128This is derived from the mild identity via `IsStokesMildTraj.stokesODE`. -/
129theorem rs_implies_global_regularity_2d_stokesODECoeffBound
130 (Hbounds : UniformBoundsHypothesis)
131 (Hconv : ConvergenceHypothesis Hbounds)
132 (ν : ℝ)
133 (hMild :
134 ∀ N : ℕ, ∀ t ≥ 0, ∀ k : Mode2,
135 (extendByZero (Hbounds.uN N t) k) =
136 (heatFactor ν t k) • (extendByZero (Hbounds.uN N 0) k)) :
137 ∃ u : ℝ → FourierState2D,
138 (∀ t : ℝ, ∀ k : Mode2,
139 Filter.Tendsto (fun N : ℕ => (extendByZero (Hbounds.uN N t)) k) Filter.atTop
140 (nhds ((u t) k)))
141 ∧ (∀ t ≥ 0, ∀ k : Mode2, ‖(u t) k‖ ≤ Hbounds.B)
142 ∧ IsStokesODETraj ν u := by
143 refine ⟨Hconv.u, ?_, ?_, ?_⟩
144 · simpa using Hconv.converges
145 · intro t ht k
146 simpa using (ConvergenceHypothesis.coeff_bound_of_uniformBounds (HC := Hconv) t ht k)
147 ·
148 have hm : IsStokesMildTraj ν Hconv.u :=
149 ConvergenceHypothesis.stokesMild_of_forall (HC := Hconv) (ν := ν) hMild
150 exact IsStokesMildTraj.stokesODE hm
151
152/-- Variant of the top-level theorem returning a first nonlinear (Duhamel-style) remainder identity.
153
154This uses `ConvergenceHypothesis.nsDuhamel_of_forall` to pass the identity to the limit,
155assuming the approximants satisfy the identity with remainders `D_N` that converge modewise. -/
156theorem rs_implies_global_regularity_2d_nsDuhamelCoeffBound
157 (Hbounds : UniformBoundsHypothesis)
158 (Hconv : ConvergenceHypothesis Hbounds)
159 (ν : ℝ)
160 (D_N : ℕ → ℝ → FourierState2D) (D : ℝ → FourierState2D)
161 (hD : ∀ t : ℝ, ∀ k : Mode2,
162 Filter.Tendsto (fun N : ℕ => (D_N N t) k) Filter.atTop (nhds ((D t) k)))
163 (hId :
164 ∀ N : ℕ, ∀ t ≥ 0, ∀ k : Mode2,
165 (extendByZero (Hbounds.uN N t) k) =
166 (heatFactor ν t k) • (extendByZero (Hbounds.uN N 0) k) + (D_N N t) k) :
167 ∃ u : ℝ → FourierState2D,
168 (∀ t : ℝ, ∀ k : Mode2,
169 Filter.Tendsto (fun N : ℕ => (extendByZero (Hbounds.uN N t)) k) Filter.atTop
170 (nhds ((u t) k)))
171 ∧ (∀ t ≥ 0, ∀ k : Mode2, ‖(u t) k‖ ≤ Hbounds.B)
172 ∧ IsNSDuhamelTraj ν D u := by
173 refine ⟨Hconv.u, ?_, ?_, ?_⟩
174 · simpa using Hconv.converges
175 · intro t ht k
176 simpa using (ConvergenceHypothesis.coeff_bound_of_uniformBounds (HC := Hconv) t ht k)
177 ·
178 -- Pass the Duhamel-style identity to the limit.
179 exact ConvergenceHypothesis.nsDuhamel_of_forall (HC := Hconv) (ν := ν) (D_N := D_N) (D := D) hD hId
180
181/-- Variant of the top-level theorem returning a first nonlinear (Duhamel-style) remainder identity,
182where the remainder is produced from the **Galerkin nonlinearity** via the Duhamel kernel integral.
183
184This removes the need to provide `D_N`, `D`, and the approximation identity explicitly; the only
185missing analytic ingredient is the dominated-convergence hypothesis `hDC` for the kernel integrands. -/
186theorem rs_implies_global_regularity_2d_nsDuhamelCoeffBound_galerkinKernel
187 (Hbounds : UniformBoundsHypothesis)
188 (Hconv : ConvergenceHypothesis Hbounds)
189 (ν : ℝ)
190 (Bop : (N : ℕ) → ConvectionOp N)
191 (hu :
192 ∀ N : ℕ, ∀ s : ℝ,
193 HasDerivAt (Hbounds.uN N) (galerkinNSRHS (N := N) ν (Bop N) (Hbounds.uN N s)) s)
194 (hint :
195 ∀ N : ℕ, ∀ t : ℝ, ∀ k : Mode2,
196 IntervalIntegrable (fun s : ℝ =>
197 (Real.exp (-(ν * (-kSq k)) * s)) • (extendByZero ((Bop N) (Hbounds.uN N s) (Hbounds.uN N s)) k))
198 MeasureTheory.volume 0 t)
199 (F : ℝ → FourierState2D)
200 (hDC :
201 ∀ t : ℝ, ∀ k : Mode2,
202 DuhamelKernelDominatedConvergenceAt ν
203 (fun N : ℕ => fun s : ℝ => extendByZero ((Bop N) (Hbounds.uN N s) (Hbounds.uN N s))) F t k) :
204 ∃ u : ℝ → FourierState2D,
205 (∀ t : ℝ, ∀ k : Mode2,
206 Filter.Tendsto (fun N : ℕ => (extendByZero (Hbounds.uN N t)) k) Filter.atTop
207 (nhds ((u t) k)))
208 ∧ (∀ t ≥ 0, ∀ k : Mode2, ‖(u t) k‖ ≤ Hbounds.B)
209 ∧ IsNSDuhamelTraj ν (duhamelKernelIntegral ν F) u := by
210 classical
211 refine ⟨Hconv.u, ?_, ?_, ?_⟩
212 · simpa using Hconv.converges
213 · intro t ht k
214 simpa using (ConvergenceHypothesis.coeff_bound_of_uniformBounds (HC := Hconv) t ht k)
215 ·
216 -- Define the forcing family from the Galerkin nonlinearity.
217 let F_N : ℕ → ℝ → FourierState2D :=
218 fun N : ℕ => fun s : ℝ => extendByZero ((Bop N) (Hbounds.uN N s) (Hbounds.uN N s))
219 -- Approximant identity: derived from the Galerkin kernel lemma.
220 have hId :
221 ∀ N : ℕ, ∀ t ≥ 0, ∀ k : Mode2,
222 (extendByZero (Hbounds.uN N t) k) =
223 (heatFactor ν t k) • (extendByZero (Hbounds.uN N 0) k)
224 + (duhamelKernelIntegral ν (F_N N) t) k := by
225 intro N t _ht k
226 simpa [F_N] using
227 (galerkin_duhamelKernel_identity (N := N) (ν := ν) (B := Bop N) (u := Hbounds.uN N) (k := k) (t := t)
228 (hu := fun s => hu N s) (hint := hint N t k))
229 -- Pass the identity to the limit using the kernel/DCT wrapper.
230 have hDC' : ∀ t : ℝ, ∀ k : Mode2, DuhamelKernelDominatedConvergenceAt ν F_N F t k := by
231 intro t k
232 simpa [F_N] using hDC t k
233 exact
234 ConvergenceHypothesis.nsDuhamel_of_forall_kernelIntegral (HC := Hconv) (ν := ν)
235 (F_N := F_N) (F := F) hDC' hId
236
237/-- Same as `rs_implies_global_regularity_2d_nsDuhamelCoeffBound_galerkinKernel`, but assumes dominated
238convergence only for the **forcing** (not the kernel integrand), plus `0 ≤ ν`. -/
239theorem rs_implies_global_regularity_2d_nsDuhamelCoeffBound_galerkinKernel_of_forcing
240 (Hbounds : UniformBoundsHypothesis)
241 (Hconv : ConvergenceHypothesis Hbounds)
242 (ν : ℝ) (hν : 0 ≤ ν)
243 (Bop : (N : ℕ) → ConvectionOp N)
244 (hu :
245 ∀ N : ℕ, ∀ s : ℝ,
246 HasDerivAt (Hbounds.uN N) (galerkinNSRHS (N := N) ν (Bop N) (Hbounds.uN N s)) s)
247 (hint :
248 ∀ N : ℕ, ∀ t : ℝ, ∀ k : Mode2,
249 IntervalIntegrable (fun s : ℝ =>
250 (Real.exp (-(ν * (-kSq k)) * s)) • (extendByZero ((Bop N) (Hbounds.uN N s) (Hbounds.uN N s)) k))
251 MeasureTheory.volume 0 t)
252 (F : ℝ → FourierState2D)
253 (hF :
254 ∀ t : ℝ, t ≥ 0 → ∀ k : Mode2,
255 ForcingDominatedConvergenceAt
256 (F_N := fun N : ℕ => fun s : ℝ => extendByZero ((Bop N) (Hbounds.uN N s) (Hbounds.uN N s)))
257 (F := F) t k) :
258 ∃ u : ℝ → FourierState2D,
259 (∀ t : ℝ, ∀ k : Mode2,
260 Filter.Tendsto (fun N : ℕ => (extendByZero (Hbounds.uN N t)) k) Filter.atTop
261 (nhds ((u t) k)))
262 ∧ (∀ t ≥ 0, ∀ k : Mode2, ‖(u t) k‖ ≤ Hbounds.B)
263 ∧ IsNSDuhamelTraj ν (duhamelKernelIntegral ν F) u := by
264 classical
265 refine ⟨Hconv.u, ?_, ?_, ?_⟩
266 · simpa using Hconv.converges
267 · intro t ht k
268 simpa using (ConvergenceHypothesis.coeff_bound_of_uniformBounds (HC := Hconv) t ht k)
269 ·
270 let F_N : ℕ → ℝ → FourierState2D :=
271 fun N : ℕ => fun s : ℝ => extendByZero ((Bop N) (Hbounds.uN N s) (Hbounds.uN N s))
272 have hId :
273 ∀ N : ℕ, ∀ t ≥ 0, ∀ k : Mode2,
274 (extendByZero (Hbounds.uN N t) k) =
275 (heatFactor ν t k) • (extendByZero (Hbounds.uN N 0) k)
276 + (duhamelKernelIntegral ν (F_N N) t) k := by
277 intro N t _ht k
278 simpa [F_N] using
279 (galerkin_duhamelKernel_identity (N := N) (ν := ν) (B := Bop N) (u := Hbounds.uN N) (k := k) (t := t)
280 (hu := fun s => hu N s) (hint := hint N t k))
281 have hF' : ∀ t : ℝ, t ≥ 0 → ∀ k : Mode2, ForcingDominatedConvergenceAt (F_N := F_N) (F := F) t k := by
282 intro t ht k
283 simpa [F_N] using hF t ht k
284 exact
285 ConvergenceHypothesis.nsDuhamel_of_forall_kernelIntegral_of_forcing (HC := Hconv) (ν := ν) hν
286 (F_N := F_N) (F := F) hF' hId
287
288/-- Same as `rs_implies_global_regularity_2d_nsDuhamelCoeffBound_galerkinKernel_of_forcing`, but
289takes the more concrete `GalerkinForcingDominatedConvergenceHypothesis` for the Galerkin forcing. -/
290theorem rs_implies_global_regularity_2d_nsDuhamelCoeffBound_galerkinKernel_of_forcingHyp
291 (Hbounds : UniformBoundsHypothesis)
292 (Hconv : ConvergenceHypothesis Hbounds)
293 (ν : ℝ) (hν : 0 ≤ ν)
294 (Bop : (N : ℕ) → ConvectionOp N)
295 (hu :
296 ∀ N : ℕ, ∀ s : ℝ,
297 HasDerivAt (Hbounds.uN N) (galerkinNSRHS (N := N) ν (Bop N) (Hbounds.uN N s)) s)
298 (hint :
299 ∀ N : ℕ, ∀ t : ℝ, ∀ k : Mode2,
300 IntervalIntegrable (fun s : ℝ =>
301 (Real.exp (-(ν * (-kSq k)) * s)) • (extendByZero ((Bop N) (Hbounds.uN N s) (Hbounds.uN N s)) k))
302 MeasureTheory.volume 0 t)
303 (hForce : GalerkinForcingDominatedConvergenceHypothesis Hbounds Bop) :
304 ∃ u : ℝ → FourierState2D,
305 (∀ t : ℝ, ∀ k : Mode2,
306 Filter.Tendsto (fun N : ℕ => (extendByZero (Hbounds.uN N t)) k) Filter.atTop
307 (nhds ((u t) k)))
308 ∧ (∀ t ≥ 0, ∀ k : Mode2, ‖(u t) k‖ ≤ Hbounds.B)
309 ∧ IsNSDuhamelTraj ν (duhamelKernelIntegral ν hForce.F) u := by
310 refine
311 rs_implies_global_regularity_2d_nsDuhamelCoeffBound_galerkinKernel_of_forcing
312 (Hbounds := Hbounds) (Hconv := Hconv) (ν := ν) hν (Bop := Bop) (hu := hu) (hint := hint)
313 (F := hForce.F) ?_
314 intro t ht k
315 simpa [galerkinForcing] using (GalerkinForcingDominatedConvergenceHypothesis.forcingDCTAt (hF := hForce) t ht k)
316
317end Regularity2D
318
319end IndisputableMonolith.ClassicalBridge.Fluids
320