IndisputableMonolith.NavierStokes.RM2U.EnergyIdentity
IndisputableMonolith/NavierStokes/RM2U/EnergyIdentity.lean · 515 lines · 7 declarations
show as:
view math explainer →
1import IndisputableMonolith.NavierStokes.RM2U.Core
2import IndisputableMonolith.NavierStokes.SkewHarmGate
3
4/-!
5# RM2U.EnergyIdentity
6
7This file is the “algebraic spine” of Option A:
8
91. Define the tail-flux boundary term (already in `RM2U.Core`).
102. Use the already-proved lemma in `SkewHarmGate` to reduce
11 “tail flux vanishes at infinity” to **two integrability obligations**
12 for the boundary term and its derivative.
13
14This keeps RM2U in a form that is:
15- faithful to the manuscript, and
16- maximally friendly to Lean / proof hygiene (no hidden assumptions).
17-/
18
19namespace IndisputableMonolith
20namespace NavierStokes
21namespace RM2U
22
23open Filter MeasureTheory Set
24open scoped Topology Interval
25
26/-!
27## RM2U operator and finite-window energy identity (time-slice)
28
29The TeX manuscript (Remark `rem:Ab-energy-identity`) uses the projected radial operator
30\[
31 \mathcal{L}A := -\partial_r^2 A - \frac{2}{r}\partial_r A + \frac{6}{r^2}A
32\]
33to obtain the coercive terms
34\[
35 \int |A_r|^2 r^2 + 6\int |A|^2.
36\]
37
38In Lean we do not yet formalize the full PDE-in-time; however, the *radial integration-by-parts*
39piece is purely algebraic and can already be stated cleanly on any finite interval `[a, R]`
40with `1 < a ≤ R`.
41-/
42
43/-- The RM2U “ℓ=2” radial operator (time-slice, no time derivative / forcing packaged here). -/
44noncomputable def rm2uOp (P : RM2URadialProfile) (r : ℝ) : ℝ :=
45 (-(P.A'' r) - (2 / r) * (P.A' r) + (6 / (r ^ 2)) * (P.A r))
46
47/-- **Algebraic identity (Bet 1 derivative rewrite).**
48
49The Bet‑1 “boundary term derivative” integrand can be rewritten (for `r ≠ 0`) as the RM2U operator
50pairing minus the coercive nonnegative terms.
51
52This is useful because it eliminates `A''` from the integrability surface: instead of proving
53integrability of an expression involving `A''`, it suffices to control the pairing
54`(rm2uOp P) * A * r^2` plus the already-coercive terms `A'^2*r^2` and `A^2`. -/
55theorem bet1_boundaryTerm_deriv_integrand_eq
56 (P : RM2URadialProfile) {r : ℝ} (hr : r ≠ 0) :
57 (-(P.A' r)) * ((P.A' r) * (r ^ 2))
58 + (-P.A r) * ((P.A'' r) * (r ^ 2) + (P.A' r) * (2 * r))
59 =
60 (rm2uOp P r) * (P.A r) * (r ^ 2)
61 - (P.A' r) ^ 2 * (r ^ 2)
62 - 6 * (P.A r) ^ 2 := by
63 -- Expand `rm2uOp` and clear denominators (`r ≠ 0` on the RM2U domain `(1,∞)`).
64 simp [rm2uOp]
65 field_simp [hr]
66 ring
67
68/-- Finite-window coercive identity for the RM2U operator, with explicit boundary terms.
69
70This is the precise Lean analogue of the integration-by-parts step inside
71TeX Remark `rem:Ab-energy-identity`, but on `[a,R]` with `1 < a ≤ R`.
72
73No PDE content is used here; this is just calculus + the already-formalized skew identity.
74-/
75theorem integral_rm2uOp_mul_energy_identity
76 (P : RM2URadialProfile) {a R : ℝ}
77 (ha1 : 1 < a) (haR : a ≤ R)
78 (hA'_int : IntervalIntegrable P.A' volume a R)
79 (hV'_int :
80 IntervalIntegrable (fun x : ℝ => (2 * x) * (P.A' x) + (x ^ 2) * (P.A'' x)) volume a R)
81 (hf :
82 IntervalIntegrable
83 (fun x : ℝ => (-(P.A'' x) - (2 / x) * (P.A' x)) * (P.A x) * (x ^ 2)) volume a R)
84 (hg :
85 IntervalIntegrable
86 (fun x : ℝ => ((6 / (x ^ 2)) * (P.A x)) * (P.A x) * (x ^ 2)) volume a R) :
87 (∫ x in a..R, (rm2uOp P x) * (P.A x) * (x ^ 2)) =
88 (-(P.A R) * (R ^ 2 * P.A' R) + (P.A a) * (a ^ 2 * P.A' a))
89 + (∫ x in a..R, (P.A' x) ^ 2 * (x ^ 2))
90 + 6 * (∫ x in a..R, (P.A x) ^ 2) := by
91 -- First apply the skew identity to the `-(A'')-(2/r)A'` part.
92 have hskew :
93 (∫ x in a..R,
94 (-(P.A'' x) - (2 / x) * (P.A' x)) * (P.A x) * (x ^ 2)) =
95 (-(P.A R) * (R ^ 2 * P.A' R) + (P.A a) * (a ^ 2 * P.A' a))
96 + ∫ x in a..R, (P.A' x) ^ 2 * (x ^ 2) := by
97 -- Supply derivative hypotheses on `[a,R]` from the profile hypotheses on `(1,∞)`.
98 have ha0 : 0 < a := lt_trans (by norm_num : (0 : ℝ) < 1) ha1
99 have hA_on : ∀ x ∈ Set.uIcc a R, HasDerivAt P.A (P.A' x) x := by
100 intro x hx
101 have hx' : x ∈ Set.Icc a R := by simpa [Set.uIcc_of_le haR] using hx
102 have hx1 : x ∈ Set.Ioi (1 : ℝ) := lt_of_lt_of_le ha1 hx'.1
103 exact P.hA x hx1
104 have hA'_on : ∀ x ∈ Set.uIcc a R, HasDerivAt P.A' (P.A'' x) x := by
105 intro x hx
106 have hx' : x ∈ Set.Icc a R := by simpa [Set.uIcc_of_le haR] using hx
107 have hx1 : (1 : ℝ) < x := lt_of_lt_of_le ha1 hx'.1
108 exact P.hA' x hx1
109 -- Now apply the generalized skew identity.
110 simpa using
111 (IndisputableMonolith.NavierStokes.Radial.integral_radial_skew_identity_from
112 (A := P.A) (A' := P.A') (A'' := P.A'') (a := a) (R := R)
113 haR ha0 hA_on hA'_on hA'_int hV'_int)
114
115 -- Expand `rm2uOp` and finish by linearity: skew part + potential `6/r^2 * A` part.
116 -- Note: `(6/(r^2))*A * A * r^2 = 6 * A^2`.
117 have hpot :
118 (∫ x in a..R, ((6 / (x ^ 2)) * (P.A x)) * (P.A x) * (x ^ 2)) =
119 6 * ∫ x in a..R, (P.A x) ^ 2 := by
120 -- First rewrite the integrand pointwise to `(6 : ℝ) * (A x)^2`.
121 have hcongr :
122 (∫ x in a..R, ((6 / (x ^ 2)) * (P.A x)) * (P.A x) * (x ^ 2)) =
123 ∫ x in a..R, (6 : ℝ) * (P.A x) ^ 2 := by
124 refine (intervalIntegral.integral_congr (μ := volume)
125 (f := fun x : ℝ => ((6 / (x ^ 2)) * (P.A x)) * (P.A x) * (x ^ 2))
126 (g := fun x : ℝ => (6 : ℝ) * (P.A x) ^ 2) ?_)
127 intro x hx
128 -- On `[a,R]` we have `x ≠ 0` because `a > 0`.
129 have ha0 : 0 < a := lt_trans (by norm_num : (0 : ℝ) < 1) ha1
130 have hx' : x ∈ Set.Icc a R := by simpa [Set.uIcc_of_le haR] using hx
131 have hx0 : x ≠ 0 := ne_of_gt (lt_of_lt_of_le ha0 hx'.1)
132 field_simp [hx0]
133 -- `field_simp` already reduces this to a trivial ring identity.
134 -- Then pull the constant out of the interval integral.
135 calc
136 (∫ x in a..R, ((6 / (x ^ 2)) * (P.A x)) * (P.A x) * (x ^ 2)) =
137 ∫ x in a..R, (6 : ℝ) * (P.A x) ^ 2 := hcongr
138 _ = (6 : ℝ) * ∫ x in a..R, (P.A x) ^ 2 := by
139 simp
140
141 -- Combine: rewrite the integrand pointwise as `f + g`, then apply linearity.
142 let f : ℝ → ℝ := fun x : ℝ =>
143 (-(P.A'' x) - (2 / x) * (P.A' x)) * (P.A x) * (x ^ 2)
144 let g : ℝ → ℝ := fun x : ℝ =>
145 ((6 / (x ^ 2)) * (P.A x)) * (P.A x) * (x ^ 2)
146 have hcongr :
147 (∫ x in a..R, (rm2uOp P x) * (P.A x) * (x ^ 2)) =
148 ∫ x in a..R, f x + g x := by
149 refine intervalIntegral.integral_congr ?_
150 intro x hx
151 simp [rm2uOp, f, g, mul_add, mul_left_comm, mul_comm]
152 have hadd :
153 (∫ x in a..R, f x + g x) =
154 (∫ x in a..R, f x) + ∫ x in a..R, g x := by
155 -- `intervalIntegral.integral_add` needs the integrability hypotheses `hf` and `hg`.
156 simpa [f, g] using
157 (intervalIntegral.integral_add (μ := volume) (a := a) (b := R)
158 (f := f) (g := g) hf hg)
159
160 -- Rewrite using `hskew` and `hpot`.
161 calc
162 (∫ x in a..R, (rm2uOp P x) * (P.A x) * (x ^ 2)) = ∫ x in a..R, f x + g x := hcongr
163 _ = (∫ x in a..R, f x) + ∫ x in a..R, g x := hadd
164 _ =
165 ((-(P.A R) * (R ^ 2 * P.A' R) + (P.A a) * (a ^ 2 * P.A' a))
166 + ∫ x in a..R, (P.A' x) ^ 2 * (x ^ 2))
167 + 6 * ∫ x in a..R, (P.A x) ^ 2 := by
168 -- `hskew` rewrites `∫ f`, and `hpot` rewrites `∫ g`.
169 simp [f, g, hskew, hpot, add_assoc]
170 _ =
171 (-(P.A R) * (R ^ 2 * P.A' R) + (P.A a) * (a ^ 2 * P.A' a))
172 + (∫ x in a..R, (P.A' x) ^ 2 * (x ^ 2))
173 + 6 * (∫ x in a..R, (P.A x) ^ 2) := by
174 -- `a + b + c` is parsed as `(a + b) + c`.
175 -- `simp` may cancel the common prefix on both sides, leaving a reflexive goal.
176 simp [add_assoc]
177
178/-- If the RM2U boundary term `(-A) * (A' * r^2)` and its derivative are integrable on `(1,∞)`,
179then the tail flux vanishes at infinity.
180
181This is exactly `SkewHarmGate.Radial.zeroSkewAtInfinity_of_integrable`, re-exported in the RM2U namespace.
182-/
183theorem tailFluxVanish_of_integrable
184 (P : RM2URadialProfile)
185 (hB_int :
186 IntegrableOn (fun x : ℝ => (-P.A x) * ((P.A' x) * (x ^ 2))) (Set.Ioi (1 : ℝ)) volume)
187 (hB'_int :
188 IntegrableOn
189 (fun x : ℝ =>
190 (-(P.A' x)) * ((P.A' x) * (x ^ 2)) + (-P.A x) * ((P.A'' x) * (x ^ 2) + (P.A' x) * (2 * x)))
191 (Set.Ioi (1 : ℝ)) volume) :
192 TailFluxVanish P.A P.A' := by
193 -- Delegate to the already formalized boundary-term lemma.
194 simpa [TailFluxVanish, tailFlux] using
195 (IndisputableMonolith.NavierStokes.Radial.zeroSkewAtInfinity_of_integrable
196 (A := P.A) (A' := P.A') (A'' := P.A'')
197 (hA := P.hA) (hA' := P.hA') hB_int hB'_int)
198
199/-!
200## Remaining “algebraic spine” interface
201
202The manuscript’s RM2U block uses an energy identity for the \(\ell=2\) radial coefficient PDE:
203once the **boundary term at infinity** vanishes, one obtains a coercive \(L^2\) estimate.
204
205We do not yet encode the full PDE-in-time in Lean, but we *can* already state (and prove) the
206time-slice “coercive estimate from tail-flux vanishing” provided we explicitly assume the
207finite-window energy/forcing control needed to pass to the limit \(R\to\infty\).
208-/
209
210/-- **Energy/forcing hypothesis interface (explicit).**
211
212This packages the precise extra assumptions needed to turn the *algebraic* identity
213`integral_rm2uOp_mul_energy_identity` into the *global* coercive bound on `(1,∞)` once the
214tail-flux vanishes.
215
216In PDE terms, this is where (time-derivative + forcing) control would enter; in our time-slice
217abstraction we expose it as a uniform bound on the interval integrals of the pairing
218`(rm2uOp P) * (A) * r^2` on `[a,R]`.
219-/
220structure TailFluxVanishImpliesCoerciveHypothesisAt (P : RM2URadialProfile) (a : ℝ) : Prop where
221 ha1 : 1 < a
222 /-- Local integrability on the near-field window `(1,a]`. -/
223 hA2_local : IntegrableOn (fun r : ℝ => (P.A r) ^ 2) (Set.Ioc (1 : ℝ) a) volume
224 hA'2_local : IntegrableOn (fun r : ℝ => (P.A' r) ^ 2 * (r ^ 2)) (Set.Ioc (1 : ℝ) a) volume
225 /-- Interval-integrability assumptions to apply `integral_rm2uOp_mul_energy_identity` on `[a,R]`. -/
226 hA'_int : ∀ R : ℝ, a ≤ R → IntervalIntegrable P.A' volume a R
227 hV'_int :
228 ∀ R : ℝ, a ≤ R →
229 IntervalIntegrable (fun x : ℝ => (2 * x) * (P.A' x) + (x ^ 2) * (P.A'' x)) volume a R
230 hf :
231 ∀ R : ℝ, a ≤ R →
232 IntervalIntegrable
233 (fun x : ℝ => (-(P.A'' x) - (2 / x) * (P.A' x)) * (P.A x) * (x ^ 2)) volume a R
234 hg :
235 ∀ R : ℝ, a ≤ R →
236 IntervalIntegrable
237 (fun x : ℝ => ((6 / (x ^ 2)) * (P.A x)) * (P.A x) * (x ^ 2)) volume a R
238 /-- Uniform bound on the energy/forcing pairing on `[a,R]`. -/
239 hPairBound :
240 ∃ C : ℝ,
241 ∀ R : ℝ, a ≤ R →
242 |∫ x in a..R, (rm2uOp P x) * (P.A x) * (x ^ 2)| ≤ C
243
244/-- **Energy/forcing hypothesis interface (explicit).**
245
246This is the existential wrapper over `TailFluxVanishImpliesCoerciveHypothesisAt`, so downstream
247composition lemmas only need to pass around one hypothesis object.
248-/
249def TailFluxVanishImpliesCoerciveHypothesis (P : RM2URadialProfile) : Prop :=
250 ∃ a : ℝ, TailFluxVanishImpliesCoerciveHypothesisAt P a
251
252/-- **Theorem (time-slice coercive bound):**
253under the explicit hypothesis interface above, `TailFluxVanish` implies `CoerciveL2Bound`.
254
255This is the Lean-side replacement for the old black-box interface.
256-/
257theorem coerciveL2Bound_of_tailFluxVanish
258 (P : RM2URadialProfile)
259 (hTC : TailFluxVanishImpliesCoerciveHypothesis P)
260 (hFlux : TailFluxVanish P.A P.A') :
261 CoerciveL2Bound P := by
262 classical
263 -- Notation.
264 rcases hTC with ⟨a, hTC⟩
265 have ha1 : 1 < a := hTC.ha1
266
267 -- A uniform bound on the pairing term.
268 rcases hTC.hPairBound with ⟨C, hC⟩
269 set Ca : ℝ := |(P.A a) * (a ^ 2 * P.A' a)|
270
271 -- Tail-flux is eventually small (use radius `1` for concreteness).
272 have hTailSmall : ∀ᶠ r in Filter.atTop, |tailFlux P.A P.A' r| ≤ (1 : ℝ) := by
273 have hball : Metric.ball (0 : ℝ) (1 : ℝ) ∈ 𝓝 (0 : ℝ) := by
274 simpa using (Metric.ball_mem_nhds (0 : ℝ) (by norm_num : (0 : ℝ) < 1))
275 have h := hFlux.eventually hball
276 filter_upwards [h] with r hr
277 -- `hr : tailFlux ... r ∈ ball 0 1`
278 have : |tailFlux P.A P.A' r| < (1 : ℝ) := by
279 simpa [Metric.mem_ball, Real.dist_eq] using hr
280 exact le_of_lt this
281
282 -- We will apply the improper-integral criterion with `b n = (n : ℝ)`.
283 let b : ℕ → ℝ := fun n => (n : ℝ)
284 have hb : Filter.Tendsto b Filter.atTop Filter.atTop := by
285 simpa [b] using (tendsto_natCast_atTop_atTop : Filter.Tendsto (fun n : ℕ => (n : ℝ)) Filter.atTop Filter.atTop)
286
287 have hEventually_ge_a : ∀ᶠ n in Filter.atTop, a ≤ b n := by
288 exact hb.eventually (eventually_ge_atTop a)
289
290 have hTailSmall_nat : ∀ᶠ n in Filter.atTop, |tailFlux P.A P.A' (b n)| ≤ (1 : ℝ) :=
291 hb.eventually hTailSmall
292
293 -- Helper: integrability on bounded windows `Ioc a (b n)` from differentiability (or empty if `b n ≤ a`).
294 have hIntA2_window :
295 ∀ n : ℕ, IntegrableOn (fun r : ℝ => (P.A r) ^ 2) (Set.Ioc a (b n)) volume := by
296 intro n
297 by_cases hna : b n ≤ a
298 · -- empty interval
299 -- if `b n ≤ a`, then `(a, b n]` is empty
300 simp [Set.Ioc_eq_empty_of_le hna]
301 · -- nonempty interval: use continuity on `Icc a (b n)` (since `a>1`)
302 have han : a ≤ b n := le_of_not_ge hna
303 have hcontA : ContinuousOn P.A (Set.Icc a (b n)) := by
304 intro x hx
305 have hx1 : x ∈ Set.Ioi (1 : ℝ) := lt_of_lt_of_le ha1 hx.1
306 exact (P.hA x hx1).continuousAt.continuousWithinAt
307 have hcont : ContinuousOn (fun r : ℝ => (P.A r) ^ 2) (Set.Icc a (b n)) := by
308 simpa [pow_two] using hcontA.mul hcontA
309 have hint : IntegrableOn (fun r : ℝ => (P.A r) ^ 2) (Set.Icc a (b n)) volume :=
310 hcont.integrableOn_Icc
311 exact hint.mono_set (by
312 intro x hx
313 exact ⟨le_of_lt hx.1, hx.2⟩)
314
315 have hIntA'2_window :
316 ∀ n : ℕ, IntegrableOn (fun r : ℝ => (P.A' r) ^ 2 * (r ^ 2)) (Set.Ioc a (b n)) volume := by
317 intro n
318 by_cases hna : b n ≤ a
319 ·
320 simp [Set.Ioc_eq_empty_of_le hna]
321 ·
322 have han : a ≤ b n := le_of_not_ge hna
323 have hcontA' : ContinuousOn P.A' (Set.Icc a (b n)) := by
324 intro x hx
325 have hx1 : x ∈ Set.Ioi (1 : ℝ) := lt_of_lt_of_le ha1 hx.1
326 exact (P.hA' x hx1).continuousAt.continuousWithinAt
327 have hcont : ContinuousOn (fun r : ℝ => (P.A' r) ^ 2 * (r ^ 2)) (Set.Icc a (b n)) := by
328 -- product of continuous functions on a compact interval
329 have h1 : ContinuousOn (fun r : ℝ => (P.A' r) ^ 2) (Set.Icc a (b n)) := by
330 simpa [pow_two] using hcontA'.mul hcontA'
331 have h2 : ContinuousOn (fun r : ℝ => r ^ 2) (Set.Icc a (b n)) := by
332 exact (continuous_id.pow 2).continuousOn
333 simpa [mul_assoc] using h1.mul h2
334 have hint : IntegrableOn (fun r : ℝ => (P.A' r) ^ 2 * (r ^ 2)) (Set.Icc a (b n)) volume :=
335 hcont.integrableOn_Icc
336 exact hint.mono_set (by
337 intro x hx
338 exact ⟨le_of_lt hx.1, hx.2⟩)
339
340 -- Key estimate on large windows: bounds the cumulative coercive cost on `[a, b n]`.
341 have hCoerciveBound_nat :
342 ∀ᶠ n in Filter.atTop,
343 (∫ x in a..b n, (P.A' x) ^ 2 * (x ^ 2)) + 6 * (∫ x in a..b n, (P.A x) ^ 2)
344 ≤ C + (1 : ℝ) + Ca := by
345 filter_upwards [hEventually_ge_a, hTailSmall_nat] with n han htail
346 -- Apply the finite-window identity at `R = b n`.
347 have hE :=
348 integral_rm2uOp_mul_energy_identity (P := P) (a := a) (R := b n)
349 (ha1 := ha1) (haR := han)
350 (hA'_int := hTC.hA'_int (b n) han)
351 (hV'_int := hTC.hV'_int (b n) han)
352 (hf := hTC.hf (b n) han)
353 (hg := hTC.hg (b n) han)
354 -- Rewrite the boundary term at `R` in terms of `tailFlux`.
355 have hBabs :
356 |-(P.A (b n)) * ((b n) ^ 2 * P.A' (b n)) + (P.A a) * (a ^ 2 * P.A' a)|
357 ≤ |tailFlux P.A P.A' (b n)| + Ca := by
358 -- triangle inequality + rewrite the first term as `tailFlux`
359 set x : ℝ := -(P.A (b n)) * ((b n) ^ 2 * P.A' (b n))
360 set y : ℝ := (P.A a) * (a ^ 2 * P.A' a)
361 have htri : |x + y| ≤ |x| + |y| := by
362 simpa [Real.norm_eq_abs] using (norm_add_le x y)
363 have hx : x = tailFlux P.A P.A' (b n) := by
364 simp [x, tailFlux, mul_left_comm, mul_comm]
365 have hy : |y| = Ca := by
366 simp [y, Ca]
367 -- rewrite `|x|` to `|tailFlux ...|` using `hx` (without unfolding `tailFlux` further)
368 calc
369 |-(P.A (b n)) * ((b n) ^ 2 * P.A' (b n)) + (P.A a) * (a ^ 2 * P.A' a)|
370 = |x + y| := by simp [x, y]
371 _ ≤ |x| + |y| := htri
372 _ = |tailFlux P.A P.A' (b n)| + Ca := by simp [hx, hy]
373 -- Bound the pairing term by `C`.
374 have hpair : |∫ x in a..b n, (rm2uOp P x) * (P.A x) * (x ^ 2)| ≤ C :=
375 hC (b n) han
376 -- Now rearrange `hE` to isolate the coercive sum, then bound by abs-values.
377 have hsum :
378 (∫ x in a..b n, (P.A' x) ^ 2 * (x ^ 2)) + 6 * (∫ x in a..b n, (P.A x) ^ 2) =
379 (∫ x in a..b n, (rm2uOp P x) * (P.A x) * (x ^ 2))
380 - (-(P.A (b n)) * ((b n) ^ 2 * P.A' (b n)) + (P.A a) * (a ^ 2 * P.A' a)) := by
381 linarith [hE]
382 -- Use `x - y ≤ |x| + |y|`.
383 have hsub_le :
384 (∫ x in a..b n, (rm2uOp P x) * (P.A x) * (x ^ 2))
385 - (-(P.A (b n)) * ((b n) ^ 2 * P.A' (b n)) + (P.A a) * (a ^ 2 * P.A' a))
386 ≤ |∫ x in a..b n, (rm2uOp P x) * (P.A x) * (x ^ 2)|
387 + |-(P.A (b n)) * ((b n) ^ 2 * P.A' (b n)) + (P.A a) * (a ^ 2 * P.A' a)| := by
388 -- `x - y = x + (-y)` and each term is bounded by its absolute value.
389 set x : ℝ := ∫ x in a..b n, (rm2uOp P x) * (P.A x) * (x ^ 2)
390 set y : ℝ := (-(P.A (b n)) * ((b n) ^ 2 * P.A' (b n)) + (P.A a) * (a ^ 2 * P.A' a))
391 have h1 : x ≤ |x| := le_abs_self x
392 have h2 : -y ≤ |y| := by
393 simpa [abs_neg] using (le_abs_self (-y))
394 -- add the inequalities and unfold `x,y`
395 simpa [x, y, sub_eq_add_neg, add_assoc] using add_le_add h1 h2
396 -- Put everything together.
397 calc
398 (∫ x in a..b n, (P.A' x) ^ 2 * (x ^ 2)) + 6 * (∫ x in a..b n, (P.A x) ^ 2)
399 = (∫ x in a..b n, (rm2uOp P x) * (P.A x) * (x ^ 2))
400 - (-(P.A (b n)) * ((b n) ^ 2 * P.A' (b n)) + (P.A a) * (a ^ 2 * P.A' a)) := hsum
401 _ ≤ |∫ x in a..b n, (rm2uOp P x) * (P.A x) * (x ^ 2)|
402 + |-(P.A (b n)) * ((b n) ^ 2 * P.A' (b n)) + (P.A a) * (a ^ 2 * P.A' a)| := hsub_le
403 _ ≤ C + (|tailFlux P.A P.A' (b n)| + Ca) := by
404 gcongr
405 _ ≤ C + ((1 : ℝ) + Ca) := by
406 gcongr
407 _ = C + (1 : ℝ) + Ca := by ring
408
409 -- From the coercive-sum bound we get separate bounds for `A^2` and `(A')^2*r^2`.
410 have hA2_bound :
411 ∀ᶠ n in Filter.atTop, (∫ x in a..b n, (P.A x) ^ 2) ≤ (C + (1 : ℝ) + Ca) / 6 := by
412 filter_upwards [hEventually_ge_a, hCoerciveBound_nat] with n han hsum
413 have hnonneg :
414 0 ≤ ∫ x in a..b n, (P.A' x) ^ 2 * (x ^ 2) := by
415 refine intervalIntegral.integral_nonneg_of_forall (μ := volume) han ?_
416 intro x
417 exact mul_nonneg (sq_nonneg (P.A' x)) (sq_nonneg x)
418 have hIA6 :
419 6 * (∫ x in a..b n, (P.A x) ^ 2)
420 ≤ C + (1 : ℝ) + Ca := by
421 -- `6*IA ≤ IAprime + 6*IA ≤ bound`
422 have : 6 * (∫ x in a..b n, (P.A x) ^ 2)
423 ≤ (∫ x in a..b n, (P.A' x) ^ 2 * (x ^ 2)) + 6 * (∫ x in a..b n, (P.A x) ^ 2) := by
424 linarith
425 exact le_trans this hsum
426 -- divide by 6
427 have hpos : (0 : ℝ) < 6 := by norm_num
428 nlinarith
429
430 have hA'2_bound :
431 ∀ᶠ n in Filter.atTop, (∫ x in a..b n, (P.A' x) ^ 2 * (x ^ 2)) ≤ C + (1 : ℝ) + Ca := by
432 filter_upwards [hEventually_ge_a, hCoerciveBound_nat] with n han hsum
433 have hnonneg :
434 0 ≤ ∫ x in a..b n, (P.A x) ^ 2 := by
435 exact intervalIntegral.integral_nonneg_of_forall (μ := volume) han (fun _ => sq_nonneg _)
436 have : (∫ x in a..b n, (P.A' x) ^ 2 * (x ^ 2))
437 ≤ (∫ x in a..b n, (P.A' x) ^ 2 * (x ^ 2)) + 6 * (∫ x in a..b n, (P.A x) ^ 2) := by
438 linarith
439 exact le_trans this hsum
440
441 -- Upgrade bounded interval-integrals to integrability on `(a,∞)`.
442 have hA2_Ioi_a :
443 IntegrableOn (fun r : ℝ => (P.A r) ^ 2) (Set.Ioi a) volume := by
444 refine MeasureTheory.integrableOn_Ioi_of_intervalIntegral_norm_bounded
445 (μ := volume) (l := Filter.atTop) (b := b) (I := (C + (1 : ℝ) + Ca) / 6) (a := a)
446 (hfi := ?_) (hb := hb) (h := ?_)
447 · intro n
448 -- `Ioc a (b n) ⊆ Ioc a (b n)`; use the window lemma
449 simpa [MeasureTheory.IntegrableOn] using (hIntA2_window n)
450 · -- bound on the norm interval integral (eventually)
451 filter_upwards [hEventually_ge_a, hA2_bound] with n han hbd
452 -- `‖(A^2)‖ = A^2` pointwise
453 have hnorm :
454 (∫ x in a..b n, ‖(P.A x) ^ 2‖ ∂volume) = ∫ x in a..b n, (P.A x) ^ 2 := by
455 refine intervalIntegral.integral_congr ?_
456 intro x hx
457 simp [Real.norm_eq_abs]
458 simpa [hnorm] using hbd
459
460 have hA'2_Ioi_a :
461 IntegrableOn (fun r : ℝ => (P.A' r) ^ 2 * (r ^ 2)) (Set.Ioi a) volume := by
462 refine MeasureTheory.integrableOn_Ioi_of_intervalIntegral_norm_bounded
463 (μ := volume) (l := Filter.atTop) (b := b) (I := (C + (1 : ℝ) + Ca)) (a := a)
464 (hfi := ?_) (hb := hb) (h := ?_)
465 · intro n
466 simpa [MeasureTheory.IntegrableOn] using (hIntA'2_window n)
467 · filter_upwards [hEventually_ge_a, hA'2_bound] with n han hbd
468 have hnorm :
469 (∫ x in a..b n, ‖(P.A' x) ^ 2 * (x ^ 2)‖ ∂volume) =
470 ∫ x in a..b n, (P.A' x) ^ 2 * (x ^ 2) := by
471 refine intervalIntegral.integral_congr ?_
472 intro x hx
473 simp [Real.norm_eq_abs]
474 simpa [hnorm] using hbd
475
476 -- Combine near-field `(1,a]` with tail `(a,∞)` to get integrability on `(1,∞)`.
477 have hA2_Ioi1 :
478 IntegrableOn (fun r : ℝ => (P.A r) ^ 2) (Set.Ioi (1 : ℝ)) volume := by
479 have hunion : Set.Ioc (1 : ℝ) a ∪ Set.Ioi a = Set.Ioi (1 : ℝ) := by
480 ext x
481 constructor
482 · intro hx
483 rcases hx with hx | hx
484 · exact hx.1
485 · exact lt_trans ha1 hx
486 · intro hx
487 by_cases hxa : x ≤ a
488 · exact Or.inl ⟨hx, hxa⟩
489 · exact Or.inr (lt_of_not_ge hxa)
490 -- use `IntegrableOn.union`
491 have := (hTC.hA2_local.union hA2_Ioi_a)
492 simpa [hunion] using this
493
494 have hA'2_Ioi1 :
495 IntegrableOn (fun r : ℝ => (P.A' r) ^ 2 * (r ^ 2)) (Set.Ioi (1 : ℝ)) volume := by
496 have hunion : Set.Ioc (1 : ℝ) a ∪ Set.Ioi a = Set.Ioi (1 : ℝ) := by
497 ext x
498 constructor
499 · intro hx
500 rcases hx with hx | hx
501 · exact hx.1
502 · exact lt_trans ha1 hx
503 · intro hx
504 by_cases hxa : x ≤ a
505 · exact Or.inl ⟨hx, hxa⟩
506 · exact Or.inr (lt_of_not_ge hxa)
507 have := (hTC.hA'2_local.union hA'2_Ioi_a)
508 simpa [hunion] using this
509
510 exact ⟨hA2_Ioi1, hA'2_Ioi1⟩
511
512end RM2U
513end NavierStokes
514end IndisputableMonolith
515