IndisputableMonolith.NavierStokes.SkewHarmGate
IndisputableMonolith/NavierStokes/SkewHarmGate.lean · 461 lines · 6 declarations
show as:
view math explainer →
1import Mathlib
2
3/-!
4# Navier–Stokes “skew / harmonic tail” gate: Lean lemmas
5
6This file is meant to support the two analytic steps that show up repeatedly in
7`navier-dec-12-rewrite.tex`:
8
91. **Skew/self-adjoint cancellations** coming from integration by parts (no “bad boundary term”);
102. **Harmonic/affine tail mode bookkeeping**, where the only obstruction is a boundary term at
11 infinity.
12
13At the moment we formalize the *integration-by-parts / boundary-term* algebra cleanly.
14The hard “tail decay ⇒ boundary term vanishes” is left as an explicit `Tendsto` hypothesis,
15matching the TeX “bad tail violates Zero-Skew at infinity” language.
16-/
17
18namespace IndisputableMonolith
19namespace NavierStokes
20
21open scoped Topology Interval BigOperators
22
23open MeasureTheory Set
24
25namespace Radial
26
27/-!
28## Weighted radial integration-by-parts identity
29
30This packages the elementary identity behind TeX Remark “Energy identity behind the coercive
31bound”:
32
33Let `A` satisfy `A' = dA/dr` and `A'' = d²A/dr²`. Define `V(r) = r² A'(r)`. Then
34
35`(-A''(r) - (2/r)A'(r)) A(r) r² = (-A(r)) * V'(r)`
36
37so integration-by-parts yields an identity with a boundary term
38`r² A(r) A'(r)` evaluated at the endpoints.
39-/
40
41section
42
43variable {A A' A'' : ℝ → ℝ} {a b : ℝ}
44
45private lemma hasDerivAt_rpow_two (r : ℝ) : HasDerivAt (fun x : ℝ => x ^ 2) (2 * r) r := by
46 -- `d/dr (r^2) = 2r`
47 simpa using ((hasDerivAt_id r).pow 2)
48
49private lemma hasDerivAt_rsq_mul (x : ℝ)
50 (hA' : HasDerivAt A' (A'' x) x) :
51 HasDerivAt (fun t : ℝ => (t ^ 2) * (A' t)) ((2 * x) * (A' x) + (x ^ 2) * (A'' x)) x := by
52 -- product rule for `(x^2) * A'(x)`
53 have hpow : HasDerivAt (fun t : ℝ => t ^ 2) (2 * x) x := hasDerivAt_rpow_two (r := x)
54 simpa [mul_assoc, add_comm, add_left_comm, add_assoc] using hpow.mul hA'
55
56end
57
58/-!
59### Finite-interval skew cancellation
60
61This is the clean “no cross term” identity on a finite interval.
62-/
63
64section Finite
65
66variable {A A' A'' : ℝ → ℝ} {R : ℝ}
67
68lemma integral_radial_skew_identity
69 (hR : 1 ≤ R)
70 (hA : ∀ x ∈ Set.uIcc (1 : ℝ) R, HasDerivAt A (A' x) x)
71 (hA' : ∀ x ∈ Set.uIcc (1 : ℝ) R, HasDerivAt A' (A'' x) x)
72 (hA'_int : IntervalIntegrable A' volume (1 : ℝ) R)
73 (hV'_int :
74 IntervalIntegrable (fun x : ℝ => (2 * x) * (A' x) + (x ^ 2) * (A'' x)) volume (1 : ℝ) R) :
75 (∫ x in (1 : ℝ)..R,
76 (-(A'' x) - (2 / x) * (A' x)) * (A x) * (x ^ 2)) =
77 (-(A R) * (R ^ 2 * A' R) + (A 1) * (1 ^ 2 * A' 1))
78 + ∫ x in (1 : ℝ)..R, (A' x) ^ 2 * (x ^ 2) := by
79 -- Apply integration by parts to `u = -A` and `v = (x^2)A'`.
80 have hu :
81 ∀ x ∈ Set.uIcc (1 : ℝ) R, HasDerivAt (fun y => -A y) (-(A' x)) x := by
82 intro x hx
83 simpa using (hA x hx).neg
84
85 have hv :
86 ∀ x ∈ Set.uIcc (1 : ℝ) R,
87 HasDerivAt (fun y : ℝ => (y ^ 2) * (A' y))
88 ((2 * x) * (A' x) + (x ^ 2) * (A'' x)) x := by
89 intro x hx
90 exact hasDerivAt_rsq_mul (A' := A') (A'' := A'') x (hA' x hx)
91
92 -- The `IntervalIntegrable` hypothesis for `u'` is inherited from `A'`.
93 have hu'_int : IntervalIntegrable (fun x : ℝ => -(A' x)) volume (1 : ℝ) R := by
94 simpa using hA'_int.neg
95
96 have hv'_int :
97 IntervalIntegrable (fun x : ℝ => (2 * x) * (A' x) + (x ^ 2) * (A'' x)) volume (1 : ℝ) R :=
98 hV'_int
99
100 -- Integration by parts.
101 have hparts :=
102 intervalIntegral.integral_mul_deriv_eq_deriv_mul (a := (1 : ℝ)) (b := R)
103 (u := fun x => -A x) (v := fun x : ℝ => (x ^ 2) * (A' x))
104 (u' := fun x => -(A' x))
105 (v' := fun x : ℝ => (2 * x) * (A' x) + (x ^ 2) * (A'' x))
106 hu hv hu'_int hv'_int
107
108 -- Rewrite the LHS into the TeX integrand, and simplify the RHS.
109 -- `(-A) * v' = (-(A'' ) - (2/x) A') * A * x^2`
110 -- and `-(u')*v = (A')*(x^2*A') = (A')^2*x^2`.
111 -- Also simplify the boundary terms at `x=1` (note `1^2 = 1`, kept as-is for clarity).
112 have : (∫ x in (1 : ℝ)..R, (-A x) * ((2 * x) * (A' x) + (x ^ 2) * (A'' x))) =
113 ∫ x in (1 : ℝ)..R, (-(A'' x) - (2 / x) * (A' x)) * (A x) * (x ^ 2) := by
114 -- pointwise algebra inside the integral
115 refine intervalIntegral.integral_congr ?_
116 intro x hx
117 -- hx : x ∈ Set.uIcc 1 R (so x ≠ 0); we only need algebra.
118 have hx0 : x ≠ 0 := by
119 -- since `1 ≤ R`, membership in `uIcc 1 R` implies `x ≥ 0` and in fact `x ≥ 1` or `x ≤ 1`;
120 -- either way `x = 0` is impossible because `0 ∉ uIcc 1 R`.
121 -- Use a simple order argument:
122 have : x ∈ Set.Icc (min (1 : ℝ) R) (max (1 : ℝ) R) := by
123 simpa [Set.uIcc] using hx
124 have hxlo : min (1 : ℝ) R ≤ x := this.1
125 -- `min 1 R ≤ x` and `min 1 R ≥ 0` hence `x ≠ 0` unless both are 0, impossible.
126 have hminpos : 0 < min (1 : ℝ) R := by
127 have : 0 < (1 : ℝ) := by norm_num
128 have hR0 : 0 < R := lt_of_lt_of_le (by norm_num : (0 : ℝ) < 1) hR
129 -- `min 1 R` is positive since both are positive
130 exact lt_min this hR0
131 exact ne_of_gt (lt_of_lt_of_le hminpos hxlo)
132 -- now just ring-ish simplification
133 field_simp [hx0]
134 ring
135
136 -- Use the rewritten version of `hparts` and finish.
137 -- Start from `hparts` and substitute the LHS.
138 -- hparts:
139 -- ∫ u * v' = u b * v b - u a * v a - ∫ u' * v
140 -- for u=-A, v=x^2*A'.
141 -- Move everything to match our target statement.
142 -- We'll rewrite `∫ u' * v` and the boundary terms.
143 calc
144 (∫ x in (1 : ℝ)..R, (-(A'' x) - (2 / x) * (A' x)) * (A x) * (x ^ 2)) =
145 (∫ x in (1 : ℝ)..R, (-A x) * ((2 * x) * (A' x) + (x ^ 2) * (A'' x))) := by
146 -- `this` was proved in the forward direction; use symmetry here.
147 simpa using this.symm
148 _ =
149 (-A R) * ((R ^ 2) * (A' R))
150 - (-A 1) * ((1 ^ 2) * (A' 1))
151 - ∫ x in (1 : ℝ)..R, (-(A' x)) * ((x ^ 2) * (A' x)) := by
152 simpa using hparts
153 _ =
154 (-(A R) * (R ^ 2 * A' R) + (A 1) * (1 ^ 2 * A' 1))
155 + ∫ x in (1 : ℝ)..R, (A' x) ^ 2 * (x ^ 2) := by
156 -- boundary terms + integral algebra
157 -- First simplify signs in boundary terms.
158 -- Then `- ∫ (-(A'))*(x^2*A') = + ∫ (A')*(x^2*A') = ∫ (A')^2 * x^2`.
159 have h_int :
160 -(∫ x in (1 : ℝ)..R, (-(A' x)) * (x ^ 2 * A' x)) =
161 ∫ x in (1 : ℝ)..R, (A' x) ^ 2 * (x ^ 2) := by
162 -- simplify under the integral
163 simp [pow_two, mul_left_comm, mul_comm]
164 -- Now rewrite the whole expression.
165 -- We keep `1^2` explicit to mirror the TeX boundary term at r=1.
166 -- Use `ring` for scalar algebra outside integrals.
167 -- Note: `simp` won't rewrite `a - b - c` to `(-a*b + ...) + ...` automatically.
168 -- We'll do it stepwise.
169 -- Start: (-A R)*... - (-A 1)*... - integral
170 -- = (-(A R)*...) + (A 1*...) + ( - integral )
171 -- then substitute `h_int`.
172 calc
173 (-A R) * (R ^ 2 * A' R) - (-A 1) * (1 ^ 2 * A' 1)
174 - ∫ x in (1 : ℝ)..R, (-(A' x)) * (x ^ 2 * A' x)
175 =
176 (-(A R) * (R ^ 2 * A' R) + (A 1) * (1 ^ 2 * A' 1))
177 + (-(∫ x in (1 : ℝ)..R, (-(A' x)) * (x ^ 2 * A' x))) := by
178 ring
179 _ =
180 (-(A R) * (R ^ 2 * A' R) + (A 1) * (1 ^ 2 * A' 1))
181 + (∫ x in (1 : ℝ)..R, (A' x) ^ 2 * (x ^ 2)) := by
182 -- reduce the second summand using `h_int`, then clean up the remaining algebra
183 have hmul :
184 (∫ x in (1 : ℝ)..R, A' x * (x ^ 2 * A' x)) =
185 ∫ x in (1 : ℝ)..R, (A' x) ^ 2 * (x ^ 2) := by
186 -- pointwise: `A' * (x^2 * A') = (A')^2 * x^2`
187 refine intervalIntegral.integral_congr ?_
188 intro x hx
189 simp [pow_two, mul_left_comm, mul_comm]
190 -- `h_int` rewrites the negated integral; then rewrite the remaining integral
191 -- via `hmul`.
192 simp [hmul]
193
194end Finite
195
196/-!
197### Finite-interval skew cancellation (general lower cutoff)
198
199This is the same identity as `integral_radial_skew_identity`, but on an interval `[a, R]`
200with a general lower endpoint `a`. This is useful for RM2U-style arguments because the
201radial coefficient PDE/ODE is naturally formulated on `(1, ∞)` and we may not want to
202assume differentiability at `r = 1`.
203-/
204
205section FiniteFrom
206
207variable {A A' A'' : ℝ → ℝ} {a R : ℝ}
208
209lemma integral_radial_skew_identity_from
210 (haR : a ≤ R)
211 (ha0 : 0 < a)
212 (hA : ∀ x ∈ Set.uIcc a R, HasDerivAt A (A' x) x)
213 (hA' : ∀ x ∈ Set.uIcc a R, HasDerivAt A' (A'' x) x)
214 (hA'_int : IntervalIntegrable A' volume a R)
215 (hV'_int :
216 IntervalIntegrable (fun x : ℝ => (2 * x) * (A' x) + (x ^ 2) * (A'' x)) volume a R) :
217 (∫ x in a..R,
218 (-(A'' x) - (2 / x) * (A' x)) * (A x) * (x ^ 2)) =
219 (-(A R) * (R ^ 2 * A' R) + (A a) * (a ^ 2 * A' a))
220 + ∫ x in a..R, (A' x) ^ 2 * (x ^ 2) := by
221 -- Apply integration by parts to `u = -A` and `v = (x^2)A'`.
222 have hu :
223 ∀ x ∈ Set.uIcc a R, HasDerivAt (fun y => -A y) (-(A' x)) x := by
224 intro x hx
225 simpa using (hA x hx).neg
226
227 have hv :
228 ∀ x ∈ Set.uIcc a R,
229 HasDerivAt (fun y : ℝ => (y ^ 2) * (A' y))
230 ((2 * x) * (A' x) + (x ^ 2) * (A'' x)) x := by
231 intro x hx
232 exact hasDerivAt_rsq_mul (A' := A') (A'' := A'') x (hA' x hx)
233
234 -- The `IntervalIntegrable` hypothesis for `u'` is inherited from `A'`.
235 have hu'_int : IntervalIntegrable (fun x : ℝ => -(A' x)) volume a R := by
236 simpa using hA'_int.neg
237
238 -- Integration by parts.
239 have hparts :=
240 intervalIntegral.integral_mul_deriv_eq_deriv_mul (a := a) (b := R)
241 (u := fun x => -A x) (v := fun x : ℝ => (x ^ 2) * (A' x))
242 (u' := fun x => -(A' x))
243 (v' := fun x : ℝ => (2 * x) * (A' x) + (x ^ 2) * (A'' x))
244 hu hv hu'_int hV'_int
245
246 -- Rewrite the LHS into the TeX integrand, and simplify the RHS.
247 have :
248 (∫ x in a..R, (-A x) * ((2 * x) * (A' x) + (x ^ 2) * (A'' x))) =
249 ∫ x in a..R, (-(A'' x) - (2 / x) * (A' x)) * (A x) * (x ^ 2) := by
250 refine intervalIntegral.integral_congr ?_
251 intro x hx
252 have hx' : x ∈ Set.Icc a R := by
253 -- since `a ≤ R`, `uIcc a R = Icc a R`
254 simpa [Set.uIcc_of_le haR] using hx
255 have hx0 : x ≠ 0 := ne_of_gt (lt_of_lt_of_le ha0 hx'.1)
256 field_simp [hx0]
257 ring
258
259 -- Finish as in `integral_radial_skew_identity`.
260 calc
261 (∫ x in a..R, (-(A'' x) - (2 / x) * (A' x)) * (A x) * (x ^ 2)) =
262 (∫ x in a..R, (-A x) * ((2 * x) * (A' x) + (x ^ 2) * (A'' x))) := by
263 simpa using this.symm
264 _ =
265 (-A R) * ((R ^ 2) * (A' R))
266 - (-A a) * ((a ^ 2) * (A' a))
267 - ∫ x in a..R, (-(A' x)) * ((x ^ 2) * (A' x)) := by
268 simpa using hparts
269 _ =
270 (-(A R) * (R ^ 2 * A' R) + (A a) * (a ^ 2 * A' a))
271 + ∫ x in a..R, (A' x) ^ 2 * (x ^ 2) := by
272 -- Keep the sign bookkeeping explicit to avoid simp rewriting the statement.
273 have h_int :
274 -(∫ x in a..R, (-(A' x)) * (x ^ 2 * A' x)) =
275 ∫ x in a..R, (A' x) ^ 2 * (x ^ 2) := by
276 have hneg :
277 -(∫ x in a..R, (-(A' x)) * (x ^ 2 * A' x)) =
278 ∫ x in a..R, A' x * (x ^ 2 * A' x) := by
279 -- `(-A') * (...)` is `-(A'*(...))`, so the outer `-` cancels.
280 simp [neg_mul, intervalIntegral.integral_neg]
281 have hmul :
282 (∫ x in a..R, A' x * (x ^ 2 * A' x)) =
283 ∫ x in a..R, (A' x) ^ 2 * (x ^ 2) := by
284 refine intervalIntegral.integral_congr ?_
285 intro x hx
286 simp [pow_two, mul_left_comm, mul_comm]
287 exact hneg.trans hmul
288 calc
289 (-A R) * (R ^ 2 * A' R) - (-A a) * (a ^ 2 * A' a)
290 - ∫ x in a..R, (-(A' x)) * (x ^ 2 * A' x)
291 =
292 (-(A R) * (R ^ 2 * A' R) + (A a) * (a ^ 2 * A' a))
293 + (-(∫ x in a..R, (-(A' x)) * (x ^ 2 * A' x))) := by
294 ring
295 _ =
296 (-(A R) * (R ^ 2 * A' R) + (A a) * (a ^ 2 * A' a))
297 + (∫ x in a..R, (A' x) ^ 2 * (x ^ 2)) := by
298 -- rewrite the last term using `h_int`
299 exact congrArg
300 (fun t => (-(A R) * (R ^ 2 * A' R) + (A a) * (a ^ 2 * A' a)) + t) h_int
301
302end FiniteFrom
303
304/-!
305### Improper-interval version (boundary term at ∞ explicit)
306
307This is the direct Lean formalization of the “bad tail violates Zero-Skew at infinity” statement:
308the only extra hypothesis needed to run the same integration-by-parts on `(1, ∞)` is a
309`Tendsto (u*v) atTop (𝓝 b')` condition. Setting `b' = 0` is exactly the **Zero-Skew at infinity**
310condition in this one-dimensional reduction.
311-/
312
313section Ioi
314
315variable {A A' A'' : ℝ → ℝ} {a' b' : ℝ}
316
317/-!
318### Deriving the “Zero-Skew at infinity” condition from integrability
319
320Mathlib already contains a very useful lemma:
321`MeasureTheory.tendsto_zero_of_hasDerivAt_of_integrableOn_Ioi`.
322
323In our setting, the *boundary term* is the scalar function
324
325`B(r) := (-A(r)) * (r^2 * A'(r))`.
326
327If `B` and `B'` are integrable on `(1,∞)`, then `B(r) → 0` as `r → ∞`.
328This is precisely the Lean form of “Zero-Skew at infinity”.
329-/
330
331lemma zeroSkewAtInfinity_of_integrable
332 (hA : ∀ x ∈ Set.Ioi (1 : ℝ), HasDerivAt A (A' x) x)
333 (hA' : ∀ x ∈ Set.Ioi (1 : ℝ), HasDerivAt A' (A'' x) x)
334 (hB_int :
335 IntegrableOn (fun x : ℝ => (-A x) * ((A' x) * (x ^ 2))) (Set.Ioi (1 : ℝ)) volume)
336 (hB'_int :
337 IntegrableOn
338 (fun x : ℝ =>
339 (-(A' x)) * ((A' x) * (x ^ 2)) + (-A x) * ((A'' x) * (x ^ 2) + (A' x) * (2 * x)))
340 (Set.Ioi (1 : ℝ)) volume) :
341 Filter.Tendsto (fun x : ℝ => (-A x) * ((A' x) * (x ^ 2))) Filter.atTop (𝓝 0) := by
342 -- Use the Mathlib lemma with `f = (-A) * (x^2*A')`.
343 have hderiv :
344 ∀ x ∈ Set.Ioi (1 : ℝ),
345 HasDerivAt (fun x : ℝ => (-A x) * ((A' x) * (x ^ 2)))
346 ((-(A' x)) * ((A' x) * (x ^ 2)) + (-A x) * ((A'' x) * (x ^ 2) + (A' x) * (2 * x))) x := by
347 intro x hx
348 have hu : HasDerivAt (fun y => -A y) (-(A' x)) x := by
349 simpa using (hA x hx).neg
350 have hv : HasDerivAt (fun y : ℝ => (A' y) * (y ^ 2)) ((A'' x) * (x ^ 2) + (A' x) * (2 * x)) x := by
351 have hA'x : HasDerivAt A' (A'' x) x := hA' x hx
352 have hpow : HasDerivAt (fun y : ℝ => y ^ 2) (2 * x) x := hasDerivAt_rpow_two (r := x)
353 -- product rule for `A'(y) * y^2`
354 simpa [mul_assoc, add_comm, add_left_comm, add_assoc] using hA'x.mul hpow
355 -- product rule
356 simpa [Pi.mul_def, mul_assoc, mul_left_comm, mul_comm, add_assoc, add_left_comm, add_comm] using hu.mul hv
357
358 -- Now apply `tendsto_zero_of_hasDerivAt_of_integrableOn_Ioi` on `(1,∞)`.
359 simpa using
360 MeasureTheory.tendsto_zero_of_hasDerivAt_of_integrableOn_Ioi (a := (1 : ℝ))
361 (f := fun x : ℝ => (-A x) * ((A' x) * (x ^ 2)))
362 (f' := fun x : ℝ =>
363 (-(A' x)) * ((A' x) * (x ^ 2)) + (-A x) * ((A'' x) * (x ^ 2) + (A' x) * (2 * x)))
364 hderiv hB'_int hB_int
365
366lemma integral_Ioi_radial_skew_identity
367 (hA : ∀ x ∈ Set.Ioi (1 : ℝ), HasDerivAt A (A' x) x)
368 (hA' : ∀ x ∈ Set.Ioi (1 : ℝ), HasDerivAt A' (A'' x) x)
369 (hUV' :
370 IntegrableOn
371 (fun x : ℝ => (-A x) * ((2 * x) * (A' x) + (x ^ 2) * (A'' x)))
372 (Set.Ioi (1 : ℝ)) volume)
373 (hU'V :
374 IntegrableOn
375 (fun x : ℝ => (-(A' x)) * ((x ^ 2) * (A' x)))
376 (Set.Ioi (1 : ℝ)) volume)
377 -- Boundary terms: right-limit at `1` and limit at infinity.
378 (h_zero :
379 Filter.Tendsto
380 (fun x : ℝ => (-A x) * ((x ^ 2) * (A' x)))
381 (𝓝[>] (1 : ℝ)) (𝓝 a'))
382 (h_infty :
383 Filter.Tendsto
384 (fun x : ℝ => (-A x) * ((x ^ 2) * (A' x)))
385 Filter.atTop (𝓝 b')) :
386 (∫ x in Set.Ioi (1 : ℝ), (-A x) * ((2 * x) * (A' x) + (x ^ 2) * (A'' x))) =
387 b' - a' + ∫ x in Set.Ioi (1 : ℝ), (A' x) ^ 2 * (x ^ 2) := by
388 -- Apply `MeasureTheory.integral_Ioi_mul_deriv_eq_deriv_mul` to
389 -- u = -A, u' = -A'
390 -- v = x^2 * A', v' = 2*x*A' + x^2*A''
391 have hu : ∀ x ∈ Set.Ioi (1 : ℝ), HasDerivAt (fun y => -A y) (-(A' x)) x := by
392 intro x hx
393 simpa using (hA x hx).neg
394
395 have hv :
396 ∀ x ∈ Set.Ioi (1 : ℝ),
397 HasDerivAt (fun y : ℝ => (y ^ 2) * (A' y))
398 ((2 * x) * (A' x) + (x ^ 2) * (A'' x)) x := by
399 intro x hx
400 exact hasDerivAt_rsq_mul (A' := A') (A'' := A'') x (hA' x hx)
401
402 have hparts :=
403 MeasureTheory.integral_Ioi_mul_deriv_eq_deriv_mul (A := ℝ) (a := (1 : ℝ))
404 (a' := a') (b' := b')
405 (u := fun x => -A x)
406 (v := fun x : ℝ => (x ^ 2) * (A' x))
407 (u' := fun x => -(A' x))
408 (v' := fun x : ℝ => (2 * x) * (A' x) + (x ^ 2) * (A'' x))
409 hu hv hUV' hU'V (by simpa [Pi.mul_def] using h_zero) (by simpa [Pi.mul_def] using h_infty)
410
411 -- `hparts` gives: ∫ u*v' = b' - a' - ∫ u'*v.
412 -- Simplify `-∫ (-(A'))*(x^2*A')` into `+∫ (A')^2*x^2`.
413 -- (We keep the overall sign convention aligned with the TeX remark.)
414 have hneg :
415 -(∫ x in Set.Ioi (1 : ℝ), (-(A' x)) * ((x ^ 2) * (A' x))) =
416 ∫ x in Set.Ioi (1 : ℝ), (A' x) ^ 2 * (x ^ 2) := by
417 -- `-(∫ -(A'*(x^2*A'))) = ∫ A'*(x^2*A') = ∫ (A')^2*x^2`
418 -- First pull the negation out of the integral.
419 -- Then simplify the integrand pointwise.
420 have :
421 -(∫ x in Set.Ioi (1 : ℝ), (-(A' x)) * ((x ^ 2) * (A' x))) =
422 ∫ x in Set.Ioi (1 : ℝ), A' x * ((x ^ 2) * (A' x)) := by
423 -- `(-A') * (...) = -(A'*(...))`, so the inner integral is `-∫ A'*(...)`,
424 -- and the outer `-` cancels it.
425 simp [neg_mul, MeasureTheory.integral_neg]
426 -- Now use the pointwise algebra `A' * (x^2 * A') = (A')^2 * x^2`.
427 -- (Associativity/commutativity is handled by `simp`.)
428 calc
429 -(∫ x in Set.Ioi (1 : ℝ), (-(A' x)) * ((x ^ 2) * (A' x))) =
430 ∫ x in Set.Ioi (1 : ℝ), A' x * ((x ^ 2) * (A' x)) := this
431 _ = ∫ x in Set.Ioi (1 : ℝ), (A' x) ^ 2 * (x ^ 2) := by
432 refine integral_congr_ae (Filter.Eventually.of_forall ?_)
433 intro x
434 simp [pow_two, mul_left_comm, mul_comm]
435
436 -- Finish.
437 -- From hparts: LHS = b' - a' - ∫ u'*v.
438 -- Replace the `- ∫ u'*v` term using `hneg`.
439 calc
440 (∫ x in Set.Ioi (1 : ℝ), (-A x) * ((2 * x) * (A' x) + (x ^ 2) * (A'' x))) =
441 b' - a' - ∫ x in Set.Ioi (1 : ℝ), (-(A' x)) * ((x ^ 2) * (A' x)) := by
442 simpa using hparts
443 _ = b' - a' + ∫ x in Set.Ioi (1 : ℝ), (A' x) ^ 2 * (x ^ 2) := by
444 -- rewrite the last term using `hneg`
445 -- `b' - a' - I = b' - a' + (-I)`
446 -- Avoid `simp` turning `(-A')*(x^2*A')` into `-(A'*(x^2*A'))` so that we can use `hneg`.
447 calc
448 b' - a' - ∫ x in Set.Ioi (1 : ℝ), (-(A' x)) * ((x ^ 2) * (A' x)) =
449 b' - a' + (-(∫ x in Set.Ioi (1 : ℝ), (-(A' x)) * ((x ^ 2) * (A' x)))) := by
450 ring
451 _ = b' - a' + ∫ x in Set.Ioi (1 : ℝ), (A' x) ^ 2 * (x ^ 2) := by
452 -- Use `hneg` as a rewrite without letting `simp` normalize the integrand.
453 simpa using congrArg (fun t => b' - a' + t) hneg
454
455end Ioi
456
457end Radial
458
459end NavierStokes
460end IndisputableMonolith
461