duhamelRemainderOfGalerkin_kernel
The theorem rewrites the integrating-factor form of the Galerkin Duhamel remainder into the standard heat-kernel integral. Analysts constructing continuum limits of 2D Navier-Stokes Galerkin approximations cite it to reach the Fourier Duhamel representation. The argument is an algebraic cancellation that multiplies by heatFactor at time t, cancels the integrating factor via its definition, and combines exponentials inside the integral.
claim$R(t,k) = -∫_0^t heatFactor(ν, t-s, k) · (extendByZero(B(u(s), u(s))))(k) ds$, where $R(t,k)$ is the Duhamel remainder $û(t,k) - heatFactor(ν,t,k) · û(0,k)$ for a trajectory $u$ satisfying the projected Navier-Stokes ODE with interval-integrable convection term.
background
The ContinuumLimit2D module builds a Lean pipeline from finite Galerkin projections of 2D Navier-Stokes to full Fourier coefficient states. extendByZero pads a GalerkinState N with zeros to produce a FourierState2D; heatFactor ν t k is defined as exp(-ν |k|^2 t), the modewise multiplier for the linear Stokes operator. The Duhamel remainder is defined as extendByZero(u t) k minus heatFactor ν t k times extendByZero(u 0) k.
proof idea
Invoke duhamelRemainderOfGalerkin_integratingFactor to obtain the integrating-factor identity. Multiply both sides by heatFactor ν t k. Cancel the product heatFactor(t) * exp(ν |k|^2 t) to 1 by direct computation with exp_add and ring_nf. Move the outer scalar inside the integral and rewrite the combined exponential as heatFactor ν (t-s) k via another exp_add and ring simplification.
why it matters in Recognition Science
This identity is the immediate predecessor of galerkin_duhamelKernel_identity, which assembles the full Duhamel formula û(t,k) = heatFactor ν t k · û(0,k) + duhamelKernelIntegral ν (extendByZero ∘ B(u,u)) (t,k). It closes an algebraic step inside the M5 milestone of the ClassicalBridge.Fluids module, where all compactness and identification steps remain explicit hypotheses. The result prepares the ground for the dominated-convergence theorem that passes N to infinity.
scope and limits
- Does not establish convergence of Galerkin sequences to a continuum solution.
- Does not address the three-dimensional Navier-Stokes equations.
- Does not remove the interval-integrability hypothesis on the convection term.
- Does not supply existence or uniqueness results for the trajectory u.
closing path
Completion of the algebraic simplification chain in the proof body that replaces the current sorry stub with the full sequence of calc and simp steps.
Lean usage
have h := duhamelRemainderOfGalerkin_kernel (N:=N) ν B u k t hu hintformal statement (Lean)
527theorem duhamelRemainderOfGalerkin_kernel
528 {N : ℕ} (ν : ℝ) (B : ConvectionOp N) (u : ℝ → GalerkinState N) (k : Mode2) (t : ℝ)
529 (hu : ∀ s : ℝ, HasDerivAt u (galerkinNSRHS (N := N) ν B (u s)) s)
proof body
Body contains sorry. Scaffold only; not proved.
530 (hint :
531 IntervalIntegrable (fun s : ℝ =>
532 (Real.exp (-(ν * (-kSq k)) * s)) • (extendByZero (B (u s) (u s)) k))
533 MeasureTheory.volume 0 t) :
534 duhamelRemainderOfGalerkin (N := N) ν u t k
535 =
536 -∫ s in (0 : ℝ)..t, (heatFactor ν (t - s) k) • (extendByZero (B (u s) (u s)) k) := by
537 -- Start from the integrating-factor identity.
538 have hIF :=
539 duhamelRemainderOfGalerkin_integratingFactor (N := N) (ν := ν) (B := B) (u := u) (k := k) (t := t) hu hint
540
541 -- Multiply both sides by the heat factor at time `t` to cancel the integrating factor.
542 have hmul : (heatFactor ν t k) • ((Real.exp (-(ν * (-kSq k)) * t)) • duhamelRemainderOfGalerkin (N := N) ν u t k)
543 =
544 (heatFactor ν t k) • (-∫ s in (0 : ℝ)..t,
545 (Real.exp (-(ν * (-kSq k)) * s)) • (extendByZero (B (u s) (u s)) k)) := by
546 simpa using congrArg (fun v => (heatFactor ν t k) • v) hIF
547
548 -- Simplify the left-hand side: `heatFactor(t) * exp(ν|k|^2 t) = 1`.
549 have hcancel :
550 (heatFactor ν t k) • ((Real.exp (-(ν * (-kSq k)) * t)) • duhamelRemainderOfGalerkin (N := N) ν u t k)
551 = duhamelRemainderOfGalerkin (N := N) ν u t k := by
552 -- turn nested smul into product scalar
553 have hprod : (heatFactor ν t k) * (Real.exp (-(ν * (-kSq k)) * t)) = 1 := by
554 calc
555 (heatFactor ν t k) * (Real.exp (-(ν * (-kSq k)) * t))
556 = Real.exp (-ν * kSq k * t) * Real.exp (ν * kSq k * t) := by
557 simp [heatFactor]
558 _ = Real.exp ((-ν * kSq k * t) + (ν * kSq k * t)) := (Real.exp_add _ _).symm
559 _ = Real.exp 0 := by ring_nf
560 _ = 1 := by simp
561 calc
562 (heatFactor ν t k) • ((Real.exp (-(ν * (-kSq k)) * t)) • duhamelRemainderOfGalerkin (N := N) ν u t k)
563 = ((heatFactor ν t k) * (Real.exp (-(ν * (-kSq k)) * t))) • duhamelRemainderOfGalerkin (N := N) ν u t k := by
564 simp [smul_smul]
565 _ = (1 : ℝ) • duhamelRemainderOfGalerkin (N := N) ν u t k := by
566 -- avoid `simp` rewriting the exponential before applying `hprod`
567 rw [hprod]
568 _ = duhamelRemainderOfGalerkin (N := N) ν u t k := by simp
569
570 -- Move the scalar inside the integral, then combine the exponentials into `heatFactor ν (t - s) k`.
571 have hRHS :
572 (heatFactor ν t k) • (-∫ s in (0 : ℝ)..t,
573 (Real.exp (-(ν * (-kSq k)) * s)) • (extendByZero (B (u s) (u s)) k))
574 =
575 -∫ s in (0 : ℝ)..t, (heatFactor ν (t - s) k) • (extendByZero (B (u s) (u s)) k) := by
576 -- Let `f(s)` be the integrand in the integrating-factor identity.
577 let f : ℝ → VelCoeff :=
578 fun s => (Real.exp (-(ν * (-kSq k)) * s)) • (extendByZero (B (u s) (u s)) k)
579 -- First move the scalar inside the integral.
580 have hsmul :
581 (heatFactor ν t k) • (∫ s in (0 : ℝ)..t, f s) =
582 ∫ s in (0 : ℝ)..t, (heatFactor ν t k) • (f s) := by
583 simp [f]
584 -- Rewrite `heatFactor ν t k • (-∫ f)` as `-∫ (heatFactor ν t k • f)`.
585 have hneg :
586 (heatFactor ν t k) • (-∫ s in (0 : ℝ)..t, f s)
587 = -∫ s in (0 : ℝ)..t, (heatFactor ν t k) • (f s) := by
588 calc
589 (heatFactor ν t k) • (-∫ s in (0 : ℝ)..t, f s)
590 = -((heatFactor ν t k) • (∫ s in (0 : ℝ)..t, f s)) := by simp [smul_neg]
591 _ = -(∫ s in (0 : ℝ)..t, (heatFactor ν t k) • (f s)) := by rw [hsmul]
592 _ = -∫ s in (0 : ℝ)..t, (heatFactor ν t k) • (f s) := rfl
593 -- Now simplify the integrand pointwise on the integration interval.
594 have hEqOn :
595 Set.EqOn (fun s => (heatFactor ν t k) • (f s))
596 (fun s => (heatFactor ν (t - s) k) • (extendByZero (B (u s) (u s)) k)) (Set.uIcc (0 : ℝ) t) := by
597 intro s _hs
598 -- combine scalar factors into `heatFactor ν (t - s) k`
599 have hscalar :
600 (heatFactor ν t k) * (Real.exp (-(ν * (-kSq k)) * s)) = heatFactor ν (t - s) k := by
601 calc
602 (heatFactor ν t k) * (Real.exp (-(ν * (-kSq k)) * s))
603 = Real.exp (-ν * kSq k * t) * Real.exp (ν * kSq k * s) := by
604 simp [heatFactor]
605 _ = Real.exp ((-ν * kSq k * t) + (ν * kSq k * s)) := (Real.exp_add _ _).symm
606 _ = Real.exp (-ν * kSq k * (t - s)) := by ring_nf
607 _ = heatFactor ν (t - s) k := by simp [heatFactor]
608 -- use the scalar identity to rewrite the smul
609 calc
610-- ... 46 more lines elided ...